proposition: Lemma arctan_correct : forall x, (IRasCR (ArcTan x) == arctan (IRasCR x))%CR.
proof: Proof. intros x. apply (ContinuousCorrect (I:proper realline)); [apply Continuous_ArcTan | | constructor]. intros q [] _. transitivity (rational_arctan q);[|apply rational_arctan_correct]. unfold arctan. pose proof (Cbind_correct QPrelengthSpace arctan_uc). apply ucEq_equiv in H. rewrite -> (H (' q))%CR. apply BindLaw1. 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