proposition: Lemma ArcTan_resp_leEq : forall x y, x[<=]y -> ArcTan x[<=]ArcTan y.
proof: Proof. intros x y Hxy. rewrite -> leEq_def. intros H. apply (leEq_less_or_equal _ _ _ Hxy). intros H0. generalize H; clear H. change (Not (ArcTan y[<]ArcTan x)). rewrite <- leEq_def. destruct H0. apply less_leEq. apply ArcTan_resp_less. assumption. stepr (ArcTan x). apply leEq_reflexive. apply ArcTan_wd. assumption. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac