Solution for Basic.triple_factoimp'
introv Hn. xwp. xapp. intros r.
xapp triple_factoimp_aux'.
{ destruct (classic (n = 0)). { left. auto. } { right. 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
