Require Export ZArith. Require Export ZArithRing. Require Export Zwf. Require Export proof_utils. Open Scope Z_scope. Definition Zfact_aux (n:Z) := Zmisc.iter n (Z*Z) (fun p => let (k,r) := p in let k' := k+1 in (k',k'*r)) (0,1). Definition Zfact (n:Z) := snd (Zfact_aux n). Theorem iter_plus : forall (x y:Z)(A:Set)(f:A->A)(v:A), 0 <= x -> 0 <= y -> iter (x+y) A f v = iter x A f (iter y A f v). intros x y; destruct x; destruct y; try (intros A f v Hcmp1 Hcmp2; unfold Zle, Zcompare in Hcmp1; unfold Zle, Zcompare in Hcmp2; ((elim Hcmp1; apply refl_equal) || (elim Hcmp2; apply refl_equal))). intros; apply refl_equal. intros; apply refl_equal. intros; apply refl_equal. unfold Zplus, iter; intros. apply iter_pos_plus. Qed. Theorem Zfact_aux_correct : forall z:Z, 0 <= z -> Zfact_aux z = (z,Z_of_nat (fact (Zabs_nat z))). induction z using (well_founded_ind (Zwf_well_founded 0)). intros zpos; destruct (Zle_lt_or_eq _ _ zpos) as [znneg|zzero]. clear zpos. assert (Heq : z = 1+(z-1)). ring. rewrite Heq. unfold Zfact_aux; rewrite iter_plus. fold (Zfact_aux (z-1)). rewrite H. rewrite Zabs_nat_plus. replace (Zabs_nat 1) with 1%nat;trivial; unfold fact, plus; fold fact. unfold iter, iter_pos. rewrite inj_mult. rewrite inj_S. rewrite Z_of_nat_Zabs_nat; unfold Zsucc. rewrite (Zplus_comm (z-1) 1); auto. omega. omega. omega. unfold Zwf; omega. omega. omega. omega. subst z. trivial. Qed. Theorem Zfact_fact_nat : forall z:Z, 0 <= z -> Zfact z = Z_of_nat(fact (Zabs_nat z)). intros z zpos; unfold Zfact; rewrite Zfact_aux_correct; auto. Qed.