proposition: Lemma DomArTanH_Dom_ArTanH : included DomArTanH (Dom ArTangH).
proof: Proof. intros x Hx. split. constructor. assert (X:Dom (([-C-][1]{+}FId){/}([-C-][1]{-}FId)) x). split. repeat constructor. split. repeat constructor. simpl. intros _. apply Greater_imp_ap. apply shift_zero_less_minus. destruct Hx; assumption. exists X. simpl. apply div_resp_pos. apply shift_zero_less_minus. destruct Hx; assumption. rstepr (x[-][--][1]). apply shift_zero_less_minus. destruct Hx; assumption. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac