Solution for Basic.triple_factoimp_aux
xwp. xapp. xif; intros C.
{ xapp. xapp. xapp. xapp. xapp. { math. } { math. }
{ rewrite facto_succ. math. math. } xsimpl. }
{ xval. xsimpl. asserts E: (i = n). { math. } subst. auto. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
