Solution for Basic.triple_factoimp
introv Hn. xwp. xapp. intros r.
xapp triple_factoimp_aux.
{ math. }
{ rewrite* facto_init. { math. } }
xapp. xapp. xval. xsimpl. auto.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
