proposition: Lemma r_pi_correct : forall r, (r_pi r == IRasCR ((inj_Q IR r)[*]Pi))%CR.
proof: Proof. intros r. unfold r_pi. repeat rewrite <- (CRmult_scale). setoid_replace (176%Z* r) with (4%Z * r * 44%Z) by (simpl; ring). setoid_replace (28%Z * r) with (4%Z * r * 7%Z) by (simpl; ring). setoid_replace (-(48)%Z * r) with (4%Z * r * -(12)%Z) by (simpl; ring). setoid_replace (96%Z * r) with (4%Z * r * 24%Z) by (simpl; ring). repeat rewrite <- CRmult_Qmult. transitivity ('4%Z * 'r *(' 44%Z * rational_arctan_small (widen_interval small_per_57) + ' 7%Z * rational_arctan_small (widen_interval small_per_239) + (' (-12)%Z * rational_arctan_small (widen_interval small_per_682) + ' 24%Z * rational_arctan_small (widen_interval small_per_12943))))%CR. ring. repeat rewrite rational_arctan_small_correct. repeat rewrite <- IR_inj_Q_as_CR. repeat (rewrite <- IR_mult_as_CR || rewrite <- IR_plus_as_CR). apply IRasCR_wd. rstepr (Four[*]inj_Q IR r[*]Pi[/]FourNZ). apply mult_wd. apply mult_wdl. apply (inj_Q_nring IR 4). eapply eq_transitive;[|apply Pi_Formula]. rstepr (nring 44[*]ArcTan (inj_Q IR (1 / 57%Z))[+] nring 7[*]ArcTan (inj_Q IR (1 / 239%Z))[+] (([--](nring 12))[*]ArcTan (inj_Q IR (1 / 682%Z))[+] nring 24[*]ArcTan (inj_Q IR (1 / 12943%Z)))). repeat apply bin_op_wd_unfolded; try apply eq_reflexive. apply (inj_Q_nring IR 44). apply (inj_Q_nring IR 7). eapply eq_transitive. apply (inj_Q_inv IR (nring 12)). csetoid_rewrite (inj_Q_nring IR 12). apply eq_reflexive. apply (inj_Q_nring IR 24). 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.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q