proposition: Lemma ArTanH_zero : forall H, ArTanH [0] H[=][0].
proof: Proof. intros H. apply mult_cancel_lft with (Two:IR). apply nringS_ap_zero. rstepr ([0]:IR). rstepl (ArTanH [0] H[+]ArTanH [0] H). assert (X:DomArTanH [--][0]). eapply iprop_wd. apply H. rational. astepl (ArTanH [0] H[+]ArTanH _ X). csetoid_rewrite (ArTanH_inv _ X H). rational. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac