proposition: Lemma Str_pth_arctanStream : forall p, Str_pth _ arctanStream p (xH, a) == (1#(1+2*p)) * ((-1)^p*a^(1+2*p))%Q.
proof: Proof. apply Pos.peano_ind. - unfold arctanStream, Str_pth, iterate, snd. rewrite Qred_correct. simpl. rewrite (Qmult_comm (1#3)), Qmult_assoc, Qmult_assoc. reflexivity. - intros p pInd. unfold Str_pth. rewrite iterate_succ. unfold Str_pth in pInd. pose proof (arctanStream_fst p) as H0. destruct (iterate _ arctanStream p (1%positive, a)) as [p0 q]. simpl in H0. subst p0. unfold snd in pInd. unfold arctanStream, snd, fst. rewrite Qred_correct. rewrite pInd. clear pInd q. rewrite <- (Qmult_comm ((-1) ^ Pos.succ p * a ^ (1 + 2 * Pos.succ p))). rewrite <- (Pos.add_1_l p). rewrite Pos2Z.inj_add, (Qpower_plus (-1)%Q). simpl ((-1)^1). rewrite Qmult_opp_1. do 5 rewrite <- (Qmult_assoc (-1)). apply (Qmult_comp (-1)). reflexivity. rewrite (Qmult_comm (1 # (1 + 2 * p))). do 5 rewrite <- (Qmult_assoc ((-1)^p)). apply (Qmult_comp ((-1)^p)). reflexivity. setoid_replace (a ^ (1 + 2 * (1 + p))) with (a ^ (1 + 2 * p) * (a * a)). do 4 rewrite <- (Qmult_assoc (a ^ (1 + 2 * p))). apply Qmult_comp. reflexivity. rewrite <- (Qmult_assoc _ a a). rewrite (Qmult_comm (1 # (1 + 2 * p))). rewrite <- (Qmult_assoc (a*a)). apply Qmult_comp. reflexivity. unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. reflexivity. rewrite <- (Qpower_plus_positive a 1 1). rewrite <- (Qpower_plus_positive a (1+2*p)). apply Qpower_positive_comp. reflexivity. rewrite <- Pos.add_assoc. apply f_equal. rewrite (Pos.add_comm 1 p). reflexivity. intro abs. discriminate. 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