proposition: Lemma Str_nth_pfactorials : forall n, nat_of_P (Str_nth n pfactorials) ≡ fact n.
proof: Proof. unfold pfactorials. intros n. pose (ONE:=1%positive). replace (fact n) with ((nat_of_P 1)*fact (pred (nat_of_P ONE) + n))%nat by (simpl;auto). replace (nat_of_P (Str_nth n (pfactorials_help 1 1))) with ((fact (pred (nat_of_P ONE)))*(nat_of_P (Str_nth n (pfactorials_help ONE 1))))%nat by (simpl; auto with * ). change (pfactorials_help 1 1) with (pfactorials_help ONE 1). generalize ONE. generalize 1%positive. unfold ONE; clear ONE. induction n. intros a b. unfold Str_nth. simpl. rewrite Nat.add_comm. now rewrite Nat.mul_comm. intros a b. unfold Str_nth in *. simpl. assert (X:=IHn (b*a)%positive (Pos.succ b)). clear IHn. rewrite nat_of_P_succ_morphism in X. rewrite <- plus_n_Sm. assert (forall (n m:nat), eq (Z_of_nat n) (Z_of_nat m) -> eq n m). { intros i j H. intuition. } apply H. clear H. apply Zmult_reg_l with (Z.of_nat (nat_of_P b)); [rewrite positive_nat_Z; auto with *|]. do 2 rewrite <- (inj_mult (nat_of_P b)). apply inj_eq. rewrite (Nat.mul_assoc (nat_of_P b) (nat_of_P a)). rewrite <- Pos2Nat.inj_mul. rewrite <- pred_Sn in X. change (S (pred (nat_of_P b) + n))%nat with (S (pred (nat_of_P b)) + n)%nat. assert (Z:S (pred (nat_of_P b)) = nat_of_P b). { apply (Nat.lt_succ_pred 0). apply Pos2Nat.is_pos. } rewrite Z. rewrite <- X. replace (fact (nat_of_P b)) with (fact (S (pred (nat_of_P b)))) by congruence. change (fact (S (pred (nat_of_P b)))) with ((S (pred (nat_of_P b)))*(fact (pred (nat_of_P b))))%nat. rewrite Z. ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams