proposition: Lemma arctanStream_fst : forall p, fst (iterate _ arctanStream p (1%positive, a)) ≡ Pos.succ (2*p).
proof: Proof. apply Pos.peano_ind. - reflexivity. - intros p H. rewrite iterate_succ. destruct (iterate (positive and Q) arctanStream p (1%positive, a)). simpl in H. subst p0. transitivity (Pos.add 2 (p~1)). reflexivity. clear q a. rewrite Pos.mul_succ_r. rewrite <- Pos.add_1_l, (Pos.add_comm 1). rewrite <- Pos.add_assoc. apply f_equal. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q Coq.Init.Datatypes