proposition: Lemma Dom_ArTanH_DomArTanH : included (Dom ArTangH) DomArTanH.
proof: Proof. intros x [_ [Hx0 Hx1]]. simpl in Hx1. assert (Hx:=Hx0). destruct Hx as [_ [_ H]]. simpl in H. assert (Hx:[1][-]x[#][0]). apply H. repeat constructor. clear H. destruct (ap_imp_less _ _ _ Hx) as [H|H]. elim (less_irreflexive IR [0]). eapply less_transitive_unfolded. apply Hx1. apply mult_cancel_less with (x[-][1]). apply inv_cancel_less. rstepl ([1][-]x). rstepr ([0]:IR). assumption. rstepr ([0][+][--][0]:IR). rstepl ([1][-]x[+][--]Two). apply plus_resp_less_both. assumption. apply inv_resp_less. apply pos_two. split. apply shift_zero_less_minus'. rstepr ([1][+]x). rstepl ([0][*]([1][-]x)). eapply shift_mult_less. assumption. apply Hx1. apply shift_zero_less_minus'. assumption. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac