proposition: Lemma arctan_uc_prf : @is_UniformlyContinuousFunction Q_as_MetricSpace CR rational_arctan Qpos2QposInf.
proof: Proof. apply (is_UniformlyContinuousFunction_wd) with rational_arctan (Qscale_modulus (1#1)). reflexivity. intros x. simpl. autorewrite with QposElim. change (/1) with 1. replace RHS with (proj1_sig x) by simpl; ring. apply Qle_refl. apply (is_UniformlyContinuousD None None I _ _ (Derivative_ArcTan I) rational_arctan). intros q [] _. apply rational_arctan_correct. intros x Hx _. assert (X:[0][<][1][+][1][*]x[*]x). apply plus_resp_pos_nonneg. apply pos_one. rstepr (x[^]2). apply sqr_nonneg. stepr ([1]:IR). simpl. apply AbsSmall_imp_AbsIR. apply leEq_imp_AbsSmall. apply shift_leEq_div. assumption. rstepl ([0]:IR). apply less_leEq; apply pos_one. apply shift_div_leEq. assumption. rstepr ([1][+]x[^]2). apply shift_leEq_plus'. rstepl ([0]:IR). apply sqr_nonneg. rstepl (nring 1:IR). apply eq_symmetric; apply (inj_Q_nring IR 1). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.Q_in_CReals CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRarctan_small CoRN.reals.fast.CRpi CoRN.transc.MoreArcTan CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.tactics.CornTac CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra Coq.micromega.Psatz