proposition: Lemma exp_ps_correct : forall (a:Q) (p:positive) H, inj_Q IR (Str_pth _ (expStream a) p (xH,1))%Q = Exp_ps (Pos.to_nat p) (inj_Q IR a) H.
proof: Proof. intros a p H. rewrite (inj_Q_wd _ _ _ (Str_pth_expStream a p)). revert p H. apply (Pos.peano_ind (fun p => ∀ (H : Dom (Exp_ps (Pos.to_nat p)) (inj_Q IR a)), inj_Q IR ((1 # Pos.of_nat (fact (Pos.to_nat p))) * a ^ p) = Exp_ps (Pos.to_nat p) (inj_Q IR a) H)). - intros H. simpl ((1 # Pos.of_nat (fact (Pos.to_nat 1))) * a ^ 1). rewrite (inj_Q_wd _ _ _ (one_mult _ a)). unfold Pos.to_nat. simpl. rewrite one_mult. setoid_replace ([1] [/] [0] [+] [1] [//] nring_fac_ap_zero IR 1) with (cr_one IR). rewrite one_mult. rewrite cg_inv_zero. reflexivity. unfold cf_div. rewrite one_mult. rewrite <- inv_one at 2. apply f_rcpcl_wd. rewrite cm_lft_unit. reflexivity. - intros p IHp H. rewrite Pos2Nat.inj_succ. stepl (([1][/](nring (S (Pos.to_nat p)))[//]nringS_ap_zero IR (Pos.to_nat p)) [*](inj_Q IR a)[*]Exp_ps (Pos.to_nat p) (inj_Q IR a) H). + simpl. rewrite (mult_commutes IR (nexp IR (Pos.to_nat p) (inj_Q IR a [-] [0]))). rewrite (ax_mult_assoc IR _ _ (cr_proof IR)). rewrite (ax_mult_assoc IR _ _ (cr_proof IR)). apply mult_wd. 2: reflexivity. rewrite cg_inv_zero. rewrite <- (mult_commutes IR (inj_Q IR a)). rewrite <- (mult_commutes IR (inj_Q IR a)). rewrite <- (ax_mult_assoc IR _ _ (cr_proof IR)). apply mult_wd. reflexivity. pose proof (mult_resp_ap_zero _ _ _ (nringS_ap_zero IR (Pos.to_nat p)) (nring_fac_ap_zero IR (Pos.to_nat p))) as X. rewrite <- (mult_of_divs _ _ _ _ _ _ _ X). apply div_wd. apply mult_one. apply eq_symmetric. change (fact (Pos.to_nat p) + (Pos.to_nat p) * fact (Pos.to_nat p))%nat with (S (Pos.to_nat p)*(fact (Pos.to_nat p)))%nat. apply nring_comm_mult. + stepl (inj_Q IR ((1#(Pos.succ p)) *a*((1 # Pos.of_nat (fact (Pos.to_nat p))) * a ^ Pos.to_nat p))%Q). * apply inj_Q_wd. rewrite <- Pos.add_1_l at 2. rewrite (Qpower_plus' a 1 p). 2: discriminate. simpl (a ^ 1). rewrite Qmult_assoc, Qmult_assoc. apply Qmult_comp. rewrite <- (Qmult_comm a), <- Qmult_assoc, Qmult_comm. apply Qmult_comp. 2: reflexivity. 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. replace (Pos.of_nat (S (Pos.to_nat p))) with (Pos.succ p). reflexivity. rewrite Nat2Pos.inj_succ. rewrite Pos2Nat.id. reflexivity. pose proof (Pos2Nat.is_pos p). intro abs. rewrite abs in H0. inversion H0. rewrite positive_nat_Z. reflexivity. * stepl (([1][/]nring (R:=IR) (S (Pos.to_nat p))[//]nringS_ap_zero IR (Pos.to_nat p))[*]inj_Q IR a[*] inj_Q IR ((1 # Pos.of_nat (fact (Pos.to_nat p))) * a ^ p)%Q) ; [apply mult_wdr; apply IHp|]. clear IHp H. apply eq_symmetric. eapply eq_transitive;[apply inj_Q_mult|]. eapply eq_transitive;[apply mult_wdl;apply inj_Q_mult|]. rewrite positive_nat_Z. apply mult_wdl. apply mult_wdl. change (1 # Pos.succ p)%Q with (1/Pos.succ p)%Q. assert (A:inj_Q IR ((Pos.succ p):Q)[=]nring (S (Pos.to_nat p))). { stepl (inj_Q IR (nring (S (Pos.to_nat p)))). apply inj_Q_nring. apply inj_Q_wd. simpl. rewrite <- Pos.add_1_r. rewrite Pos2Z.inj_add, inject_Z_plus. apply Qplus_comp. 2: reflexivity. revert p. apply Pos.peano_ind. reflexivity. intros p IHp. rewrite Pos2Nat.inj_succ. simpl. rewrite -> IHp. rewrite <- Pos.add_1_r. rewrite Pos2Z.inj_add, inject_Z_plus. reflexivity. } assert (B:inj_Q IR (Pos.succ p:Q)[#][0]). { stepl (nring (R:=IR) (S (Pos.to_nat p))). apply nringS_ap_zero. apply eq_symmetric;assumption. } eapply eq_transitive;[apply inj_Q_div|]. instantiate (1:=B). apply div_wd. apply inj_Q_One. exact A. 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