proposition: Lemma ArTanH_series_lemma2 : fun_series_convergent_IR DomArTanH (fun n : nat => Half (R:=IR){**} ((Log_ps n[o][-C-][1]{+}FId){-}(Log_ps n[o][-C-][1]{-}FId))).
proof: Proof. apply FSeries_Sum_scal_conv;[|Contin]. apply FSeries_Sum_minus_conv; apply FSeries_Sum_comp_conv with (olor [0] Two); try apply Log_series_convergent_IR; try Contin; intros a b Hab H; simpl. exists ([1][+]a); exists ([1][+]b). assert (H0:[1][+]a[<=][1][+]b). apply plus_resp_leEq_lft; assumption. exists H0. split. intros c [Hc0 Hc1]. split. eapply less_leEq_trans;[|apply Hc0]. destruct (H _ (compact_inc_lft _ _ Hab)) as [A _]. apply shift_less_plus'. rstepl ([--][1]:IR). assumption. eapply leEq_less_trans;[apply Hc1|]. rstepr ([1][+][1]:IR). apply plus_resp_less_lft. destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. assumption. intros x _ [Hx0 Hx1]. split; apply plus_resp_leEq_lft; assumption. exists ([1][-]b); exists ([1][-]a). assert (H0:[1][-]b[<=][1][-]a). apply plus_resp_leEq_lft. apply inv_resp_leEq; assumption. exists H0. split. intros c [Hc0 Hc1]. split. eapply less_leEq_trans;[|apply Hc0]. destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. apply shift_zero_less_minus. assumption. eapply leEq_less_trans;[apply Hc1|]. rstepr ([1][+][--][--][1]:IR). apply plus_resp_less_lft. apply inv_resp_less. destruct (H _ (compact_inc_lft _ _ Hab)) as [A _]. assumption. intros x _ [Hx0 Hx1]. split; apply plus_resp_leEq_lft; apply inv_resp_leEq; assumption. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac