Solution for Basic.triple_repeat_incr
intros m. induction_wf IH: (downto 0) m. unfold downto in IH.
intros n p Hm. xwp. xapp. xif; intros C.
{ xapp. xapp. xapp. { math. } { math. } xsimpl. math. }
{ xval. xsimpl. math. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
