proposition: Lemma rational_arctan_pos_correct : forall a (Ha: 0 <= a), (rational_arctan_pos Ha == IRasCR (ArcTan (inj_Q IR a)))%CR.
proof: Proof. intros a Ha. unfold rational_arctan_pos. destruct (Qle_total (2 # 5) a). destruct (Qle_total (5 # 2) a). apply rational_arctan_big_pos_correct. apply rational_arctan_mid_pos_correct. apply rational_arctan_small_correct. 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