proposition: Lemma ArTanH_series_lemma : forall n : nat, Feq DomArTanH (Half (R:=IR){**} ((Log_ps n[o][-C-][1]{+}FId){-}(Log_ps n[o][-C-][1]{-}FId))) (ArTanH_ps n).
proof: Proof. unfold Log_ps, ArTanH_ps. unfold FPowerSeries. intros n. FEQ. apply included_FScalMult. apply included_FMinus; apply included_FComp; Included; repeat constructor. simpl. change (Half (R:=IR)[*] (Log_series_coef n[*]([1][+]x[-][1])[^]n[-] Log_series_coef n[*]([1][-]x[-][1])[^]n)[=] ArTanH_series_coef n[*]nexp IR n (x[-][0])). unfold ArTanH_series_coef. destruct n as [|n]. destruct (CLogic.Even_Odd_dec 0) as [A|A]; [simpl; rational | exfalso; destruct A as [k B]; rewrite Nat.add_1_r in B; discriminate B ]. rstepl (Half (R:=IR)[*] (Log_series_coef (S n)[*](x[^]S n[-]([--]x)[^]S n))). destruct (CLogic.Even_Odd_dec (S n)) as [A|A]; unfold cg_minus. csetoid_rewrite (inv_nexp_even _ x _ A). rational. csetoid_rewrite (inv_nexp_odd _ x _ A). unfold Half. rstepl (Log_series_coef (S n)[*](x[^]S n)). apply mult_wd;[|change (x[^]S n[=](x[+][--][0])[^]S n); rational]. unfold Log_series_coef. apply div_wd; try apply eq_reflexive. apply Nat.Even_succ in A. csetoid_rewrite (inv_nexp_even IR [1] _ A). algebra. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac