proposition: Lemma rational_arctan_mid_pos_correct_aux (a : Q) : 0 < a → (r_pi (1#4) + IRasCR (ArcTan (inj_Q IR ((a - 1) / (a + 1)))))%CR = IRasCR (ArcTan (inj_Q IR a)).
proof: Proof. intros Ha. rewrite r_pi_correct. rewrite <-IR_plus_as_CR. apply IRasCR_wd. stepl (Pi[/]FourNZ[+]ArcTan (inj_Q IR ((a - 1) / (a + 1)))). csetoid_rewrite_rev (ArcTan_one). set (y:= (inj_Q IR ((a - 1) / (a + 1)))). assert (Y:[0][<][1][-][1][*]y). apply shift_zero_less_minus. rstepl y. rstepr (nring 1:IR). stepr (inj_Q IR 1); [| now apply (inj_Q_nring IR 1)]. apply inj_Q_less. now apply rational_arctan_mid_pos_prf. apply eq_transitive with (ArcTan ([1][+]y[/]_[//](Greater_imp_ap _ _ _ Y))). apply ArcTan_plus_ArcTan. apply shift_zero_leEq_minus'. rstepr (Two:IR). apply nring_nonneg. apply leEq_reflexive. rstepl ([--](nring 1:IR)). stepl (inj_Q IR ([--](1))). apply inj_Q_leEq. apply less_leEq. now apply rational_arctan_mid_pos_prf. csetoid_rewrite_rev (inj_Q_nring IR 1). apply inj_Q_inv. rstepr (nring 1:IR). stepr (inj_Q IR 1); [| now apply (inj_Q_nring IR 1)]. apply inj_Q_leEq. apply less_leEq. now apply rational_arctan_mid_pos_prf. apply ArcTan_wd. apply mult_cancel_lft with ([1][-][1][*]y). apply Greater_imp_ap; assumption. rstepl ([1][+]y). rstepr (inj_Q IR a[-]y[*]inj_Q IR a). csetoid_replace ([1]:IR) (inj_Q IR 1). unfold y. set (y' := ((a - 1) / (a + 1))). unfold cg_minus. csetoid_rewrite_rev (inj_Q_mult IR y' a). eapply eq_transitive. apply eq_symmetric; apply inj_Q_plus. apply eq_transitive with (inj_Q IR (a[+][--](y'[*]a)));[| apply inj_Q_minus]. apply inj_Q_wd. simpl. unfold y'. field. intros E. destruct (Qlt_irrefl 0). transitivity a; auto. rewrite <-E, Qlt_minus_iff. now ring_simplify. rstepl (nring 1:IR). apply eq_symmetric; apply (inj_Q_nring IR 1). apply bin_op_wd_unfolded;[|apply eq_reflexive]. apply mult_cancel_lft with Four. apply four_ap_zero. rstepl ((nring 1:IR)[*]Pi). rstepr ((Four[*]inj_Q IR (1 # 4))[*]Pi). apply mult_wdl. stepl (inj_Q IR 1); [| now apply (inj_Q_nring IR 1)]. stepr (inj_Q IR (4*(1#4))). apply inj_Q_wd. simpl. reflexivity. eapply eq_transitive. apply inj_Q_mult. apply mult_wdl. apply (inj_Q_nring IR 4). 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