proposition: Theorem factZ_fix_eqn: forall x, factZ_it x = match Z_lt_le_dec x 0 with | left h => 0 | right h => match Z.eq_dec 0 x with left h' => 1 | right h'' => x * factZ_it (x - 1) end end.
proof: Proof. intros x; unfold factZ_it; destruct (factZ_terminates x) as [v [p Heq]]; destruct (factZ_terminates (x - 1)) as [v' [p' Heq']]. rewrite <- (Heq (S ((p + p') + 1)) factZ_it). - simpl iter; unfold factZ_it_F. case (Z_lt_le_dec x 0); auto. case (Z.eq_dec 0 x); auto. rewrite <- (Heq' ((p + p') + 1)%nat factZ_it). + reflexivity. + lia. - lia. Qed.
imports: ZArith ZArithRing Zcompare Zwf Lia