proposition: Lemma ArTanH_series_convergent_IR : fun_series_convergent_IR DomArTanH ArTanH_ps.
proof: Proof. eapply fun_series_convergent_wd_IR;[|apply ArTanH_series_lemma2]. apply ArTanH_series_lemma. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac