proposition: Lemma rational_arctan_big_pos_correct_aux (a : Q) : 0 < a → (r_pi (1 # 2) - IRasCR (ArcTan (inj_Q IR (/ a))))%CR = IRasCR (ArcTan (inj_Q IR a)).
proof: Proof. intros Ha. rewrite -> r_pi_correct. assert (H1:(inj_Q IR a)[#][0]). stepr (inj_Q IR [0]); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_ap. apply (Greater_imp_ap _ a 0); assumption. rewrite <- IR_minus_as_CR. apply IRasCR_wd. stepl (Pi[/]TwoNZ[-](ArcTan ([1][/]_[//]H1))). assert (H2:[0][<]inj_Q IR a). stepl (inj_Q IR [0]); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_less; assumption. unfold cg_minus. csetoid_rewrite (ArcTan_recip _ H1 H2). rational. apply bin_op_wd_unfolded. rstepl (((nring 1)[/]TwoNZ)[*]Pi). apply mult_wdl. change (1#2) with (1/2). assert (H2:(inj_Q IR (2#1))[#][0]). stepr (inj_Q IR [0]); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_ap; discriminate. apply eq_transitive with ((inj_Q IR 1)[/]_[//]H2). apply div_wd. apply eq_symmetric; apply (inj_Q_nring IR 1). apply eq_symmetric; apply (inj_Q_nring IR 2). apply eq_symmetric; apply inj_Q_div. apply un_op_wd_unfolded. apply ArcTan_wd. apply eq_transitive with ((inj_Q IR 1)[/]_[//]H1). apply div_wd. rstepl (nring 1:IR). apply eq_symmetric; apply (inj_Q_nring IR 1). apply eq_reflexive. eapply eq_transitive. apply eq_symmetric; apply inj_Q_div. apply inj_Q_wd. simpl. unfold Qdiv. 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