Solution for Basic.triple_factoimp_aux'
xwp. xapp. xif; intros C.
{ destruct Hn as [(?&?)|?]. false. math.
xapp. xapp. xapp. xapp. xapp. { math. } { right. math. }
{ rewrite facto_succ. math. math. } xsimpl. }
{ xval. xsimpl.
{ destruct Hn as [(?&?)|?].
{ subst. rewrite facto_init; [|math].
rewrite facto_init; [|math]. auto. }
{ asserts E: (i = n). { math. } subst. auto. } } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
