proposition: Lemma ArcTan_def_lemma : Continuous realline {1/} ( [-C-][1]{+}FId{^}2).
proof: Proof. apply Continuous_recip. Contin. red in |- *; intros. split. Included. exists OneR. apply pos_one. intros; simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. apply shift_leEq_plus'. astepl ZeroR; astepr (y[^]2). apply sqr_nonneg. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT