proposition: Lemma rational_arctan_small_correct_aux (a : Q) : (- IRasCR (ArcTan (inj_Q IR (- a)%Q)))%CR = IRasCR (ArcTan (inj_Q IR a)).
proof: Proof. rewrite <- IR_opp_as_CR. apply IRasCR_wd. csetoid_rewrite_rev (ArcTan_inv (inj_Q IR (-a))). apply ArcTan_wd. eapply eq_transitive. apply eq_symmetric; apply (inj_Q_inv IR (-a)). apply inj_Q_wd. simpl. ring. 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