proposition: Lemma Str_nth_artanhSequence n : forall a, (Str_nth n (artanhSequence a) == (1#P_of_succ_nat (2*n))*a^(1+2*n)%nat)%Q.
proof: Proof. intro a. unfold artanhSequence. unfold mult_Streams. rewrite Str_nth_zipWith. rewrite Str_nth_everyOther. rewrite Str_nth_Qrecip_positives. rewrite -> (Str_nth_powers_help_int_pow _ Z.of_nat). rewrite <- Qpower_mult. rewrite inj_plus. rewrite -> (Qpower_plus' a 1 (2*n)%nat); auto with *. rewrite inj_mult. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.iso_CReals CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRGeometricSum CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qabs Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.transc.ArTanH CoRN.reals.fast.CRarctan_small CoRN.tactics.Qauto CoRN.tactics.CornTac