proposition: Lemma Str_pth_expStream : forall p, Str_pth _ expStream p (xH,1) == (1#Pos.of_nat (fact (Pos.to_nat p)))*a^p.
proof: Proof. apply Pos.peano_ind. - unfold Str_pth. simpl. apply Qmult_1_r. - intros. unfold Str_pth. rewrite iterate_succ. simpl. unfold Str_pth in H. rewrite H. clear H. rewrite expStream_fst. simpl. rewrite <- (Qmult_comm (1#Pos.succ p)), Qmult_assoc, Qmult_assoc. rewrite <- (Qmult_assoc ((1 # Pos.succ p) * (1 # Pos.of_nat (fact (Pos.to_nat p))))). apply Qmult_comp. + unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_l. rewrite Z.mul_1_l. rewrite Pos2Nat.inj_succ. change (fact (S (Pos.to_nat p)))%nat with (S (Pos.to_nat p) * fact (Pos.to_nat p))%nat. rewrite Nat2Pos.inj_mul. 2: discriminate. 2: apply fact_neq_0. rewrite Nat2Pos.inj_succ, Pos2Nat.id. reflexivity. pose proof (Pos2Nat.is_pos p). intro abs. rewrite abs in H. inversion H. + rewrite <- Pos.add_1_r. rewrite Qpower_plus_positive. reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra