proposition: Lemma ArTanH_maps_compact_lemma : maps_compacts_into DomArTanH (openl [0]) (([-C-][1]{+}FId){/}([-C-][1]{-}FId)).
proof: Proof. intros a b Hab H. assert (Ha : [0][<][1][-]a). apply shift_zero_less_minus. destruct (H _ (compact_inc_lft _ _ Hab)) as [_ A]. assumption. assert (Ha' : [1][-]a[#][0]). apply Greater_imp_ap. assumption. exists ([1][+]a[/]_[//]Ha'). assert (Hb : [0][<][1][-]b). apply shift_zero_less_minus. destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. assumption. assert (Hb' : [1][-]b[#][0]). apply Greater_imp_ap. assumption. exists ([1][+]([1][+]b[/]_[//]Hb')). assert (Hcd : ([1][+]a[/]_[//]Ha')[<]([1][+]([1][+]b[/]_[//]Hb'))). rstepl ([0][+]([1][+]a[/]_[//]Ha')). apply plus_resp_less_leEq. apply pos_one. apply shift_leEq_div; try assumption. rstepl ((([1][-]a[*]b)[+](a[-]b))[/]_[//]Ha'). apply shift_div_leEq; try assumption. rstepr (([1][-]a[*]b)[+](b[-]a)). apply plus_resp_leEq_lft. apply shift_minus_leEq. rstepr (Two[*]b[-]a). apply shift_leEq_minus. rstepl (Two[*]a). apply mult_resp_leEq_lft; try assumption. apply less_leEq; apply pos_two. exists Hcd. split. intros y [Hy _]. eapply less_leEq_trans ;[|apply Hy]. apply div_resp_pos. assumption. destruct (H _ (compact_inc_lft _ _ Hab)) as [A _]. rstepr (a[-][--][1]). apply shift_zero_less_minus. assumption. intros x Hx H0. simpl. assert ([0][<][1][-]x). destruct (H0) as [_ A]. rstepr (([1][-]b)[+](b[-]x)). rstepl ([0][+][0]:IR). apply plus_resp_less_leEq. assumption. apply shift_zero_leEq_minus. assumption. split. apply shift_leEq_div; try assumption. rstepl ((([1][-]x[*]a)[+](a[-]x))[/]_[//]Ha'). apply shift_div_leEq; try assumption. rstepr (([1][-]x[*]a)[+](x[-]a)). apply plus_resp_leEq_lft. apply shift_minus_leEq. rstepr (Two[*]x[-]a). apply shift_leEq_minus. rstepl (Two[*]a). apply mult_resp_leEq_lft; try assumption. destruct H0; assumption. apply less_leEq; apply pos_two. apply leEq_transitive with ([0][+]([1][+]b[/]_[//]Hb')). apply shift_div_leEq; try assumption. rstepr ((([1][-]x[*]b)[+](b[-]x))[/]_[//]Hb'). apply shift_leEq_div; try assumption. rstepl (([1][-]x[*]b)[+](x[-]b)). apply plus_resp_leEq_lft. apply shift_minus_leEq. rstepr (Two[*]b[-]x). apply shift_leEq_minus. rstepl (Two[*]x). apply mult_resp_leEq_lft; try assumption. destruct H0; assumption. apply less_leEq; apply pos_two. apply plus_resp_leEq. apply less_leEq; apply pos_one. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac