proposition: Lemma ArcTan_resp_less : forall x y, x[<]y -> ArcTan x[<]ArcTan y.
proof: Proof. intros x y H. unfold ArcTan. eapply (Derivative_imp_resp_less realline I). apply Derivative_ArcTan. assumption. constructor. constructor. intros contF'. set (F:={1/}([-C-][1]{+}FId{^}2):PartIR) in *. assert (Hz0:forall z:IR, [0][<][1][+][1][*]z[*]z). intros z. apply less_leEq_trans with [1]. apply pos_one. apply shift_leEq_plus'. rstepl ([0]:IR). rstepr (z[^]2). apply sqr_nonneg. assert (Hz:forall z, Dom F z). intros z. repeat constructor. simpl. intros _. apply Greater_imp_ap. apply Hz0. set (z:=Max (AbsIR x) (AbsIR y)). apply less_leEq_trans with (F z (Hz z)). simpl. apply shift_less_div. apply Hz0. rstepl ([0]:IR). apply pos_one. apply leEq_glb. simpl. intros a [Ha0 Ha1] H0. apply recip_resp_leEq. apply Hz0. clear H0 contF' F Hz. apply plus_resp_leEq_lft. apply shift_leEq_rht. rstepr ((z[-]a)[*](z[-][--]a)). unfold z. apply mult_resp_nonneg; apply shift_leEq_lft; eapply leEq_transitive. apply Ha1. apply Max_leEq; (eapply leEq_transitive;[apply leEq_AbsIR|]). apply lft_leEq_Max. apply rht_leEq_Max. apply inv_resp_leEq. apply Ha0. unfold MIN, Min. rstepl (Max [--]x [--]y). apply Max_leEq; (eapply leEq_transitive;[apply inv_leEq_AbsIR|]). apply lft_leEq_Max. apply rht_leEq_Max. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac