proposition: Lemma rational_artanh_slow_correct : forall (a:Q) Ha Ha0, (@rational_artanh_slow a Ha == IRasCR (ArTanH (inj_Q IR a) Ha0))%CR.
proof: Proof. intros a Ha Ha0. unfold rational_artanh_slow. rewrite InfiniteGeometricSum_correct'. apply IRasCR_wd. eapply eq_transitive_unfolded; [|apply (ArTanH_series (inj_Q IR a) (ArTanH_series_convergent_IR) (artanh_DomArTanH Ha) Ha0)]. simpl. unfold series_sum. apply Lim_seq_eq_Lim_subseq with Nat.double. unfold Nat.double; auto with *. intros n. exists (S n). unfold Nat.double; auto with *. intros n. simpl. clear - n. induction n. apply eq_reflexive. simpl. set (A:=nexp IR (Nat.add n (S n)) (inj_Q IR a[-][0])). rewrite Nat.add_comm. simpl. fold (Nat.double n). csetoid_rewrite_rev IHn. clear IHn. csetoid_replace (ArTanH_series_coef (Nat.double n)[*]nexp IR (Nat.double n) (inj_Q IR a[-][0])) ([0]:IR). csetoid_replace (ArTanH_series_coef (S (Nat.double n))[*]A) (inj_Q IR (Str_nth n (artanhSequence a))). rational. unfold ArTanH_series_coef. case_eq (CLogic.Even_Odd_dec (S (Nat.double n))); intros H. elim (Nat.Even_Odd_False _ H). now rewrite <-Nat.add_1_r, Nat.double_twice; exists n. intros _. eapply eq_transitive; [|apply inj_Q_wd; simpl;symmetry;apply Str_nth_artanhSequence]. eapply eq_transitive; [|apply eq_symmetric; apply inj_Q_mult]. apply mult_wd. assert (X:(inj_Q IR (nring (S (Nat.double n))))[#][0]). stepr (inj_Q IR [0]). apply inj_Q_ap. apply nringS_ap_zero. apply (inj_Q_nring IR 0). stepr (inj_Q IR (nring 1)[/]_[//]X). apply div_wd. rstepl (nring 1:IR). apply eq_symmetric. apply (inj_Q_nring IR 1). apply eq_symmetric. apply (inj_Q_nring). assert (X0:inj_Q IR (inject_Z (P_of_succ_nat (2 * n)))[#][0]). stepr (inj_Q IR [0]). apply inj_Q_ap. discriminate. apply (inj_Q_nring IR 0). eapply eq_transitive; [|apply inj_Q_wd; symmetry; apply Qmake_Qdiv]. eapply eq_transitive; [|apply eq_symmetric; apply (fun b => inj_Q_div _ b _ X0)]. apply div_wd. apply eq_reflexive. apply inj_Q_wd. rewrite <- POS_anti_convert. eapply eq_transitive;[apply nring_Q|]. unfold Nat.double. simpl. replace (n+0)%nat with n by ring. reflexivity. unfold A; clear A. eapply eq_transitive;[|apply eq_symmetric; apply inj_Q_power]. change ((inj_Q IR a[-][0])[^](n+S n)[=]inj_Q IR a[^](1 + 2 * n)). replace (n + S n)%nat with (1 + 2*n)%nat by ring. apply nexp_wd. rational. unfold ArTanH_series_coef. case_eq (CLogic.Even_Odd_dec (Nat.double n)). intros _ _. rational. intros o. elim (fun x=> Nat.Even_Odd_False _ x o). apply even_plus_n_n. 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