intros n. induction_wf IH: (downto 0) n. unfold downto in IH. intros Hn. applys triple_app_fix. { reflexivity. } simpl. applys triple_let. { applys triple_le. } intros b. simpl. apply triple_hpure'. intros ->. (* applys triple_if_case; rew_bool_eq in *. *) applys triple_if. case_if as C. { applys triple_val. xsimpl. rewrite facto_init; math. } { applys triple_let. { applys triple_sub. } intros x. simpl. applys triple_let (fun r => \[r = (facto (n-1))]). { apply triple_hpure'. intros ->. applys IH. { math. } { math. } } intros y. simpl. applys triple_hpure'. intros ->. applys triple_conseq. { applys triple_mul. } { xsimpl. } xsimpl. intros ? ->. rewrite (@facto_step n); math. } Qed.