proposition: Lemma expStream_correct : ∀ p : positive, Str_pth _ (CRexp.expStream (AQtoQ a)) p (1%positive, 1%Q) == let (_, r) := iterate _ (fS ARexpStream) p (1%positive, (1, 1)) in AQtoQ (fst r) / AQtoQ (snd r).
proof: Proof. apply Pos.peano_ind. - unfold Str_pth. simpl. rewrite Qmult_1_l, Qmult_1_r. rewrite rings.mult_1_l, rings.mult_1_l. pose proof (AQtoQ_ZtoAQ 1). unfold cast in H5. rewrite H5. unfold stdlib_rationals.inject_Z_Q, inject_Z. unfold Qdiv. rewrite Qmult_1_r. reflexivity. - intros. unfold Str_pth. rewrite iterate_succ, iterate_succ. unfold Str_pth in H5. pose proof (fS_fst ARexpStream p (1,1)). pose proof (expStream_fst (AQtoQ a) p). destruct (iterate _ (CRexp.expStream (AQtoQ a)) p (1%positive, 1%Q)) as [u v]. destruct (iterate (positive * (AQ * AQ)) (fS ARexpStream) p (1%positive, (1, 1))). unfold snd in H5 at 1. simpl. unfold fst in H6. subst p0. rewrite H5. unfold fst in H7. clear H5 v. subst u. assert (forall i j : AQ, AQtoQ (i*j) == AQtoQ i * AQtoQ j). { intros. rewrite rings.preserves_mult. reflexivity. } rewrite H5, H5. unfold Qdiv. rewrite Qinv_mult_distr. pose proof (AQtoQ_ZtoAQ). unfold cast in H6. rewrite H6. unfold stdlib_rationals.inject_Z_Q, inject_Z. setoid_replace (/ (Z.pos (Pos.succ p) # 1))%Q with (1#Pos.succ p). ring. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program MathClasses.misc.workaround_tactics CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith