proposition: Lemma ArTanH_inv : forall x Hx Hx', ArTanH [--]x Hx[=][--](ArTanH x Hx').
proof: Proof. intros x Hx Hx'. unfold ArTanH, ArTangH. generalize (DomArTanH_Dom_ArTanH). intros X. simpl in X. set (A:=(ProjT2 (Prj2 (X [--]x Hx)))). set (B:=(ProjT2 (Prj2 (X x Hx')))). change (Half (R:=IR)[*]Log _ A[=][--](Half (R:=IR)[*]Log _ B)). generalize A B. clear A B. intros A B. rstepr (Half[*][--](Log _ B)). apply mult_wdr. apply cg_inv_unique. assert (C:=mult_resp_pos _ _ _ B A). astepl (Log _ C). astepr (Log _ (pos_one IR)). apply Log_wd. rational. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac