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 ((68*r)) with ((4*r*17)) by (simpl; ring). setoid_replace (32*r) with (4*r*8) by (simpl; ring). setoid_replace (40*r) with (4*r*10) by (simpl; ring). setoid_replace (20*r) with (4*r*5) by (simpl; ring). repeat rewrite <- CRmult_Qmult. transitivity ('4 * 'r *(' 17 * rational_arctan_small (widen_interval small_per_23) + ' 8 * rational_arctan_small (widen_interval small_per_182) + (' 10 * rational_arctan_small (widen_interval small_per_5118) + ' 5 * rational_arctan_small (widen_interval small_per_6072))))%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 17[*]ArcTan (inj_Q IR (1 / 23%Z))[+] nring 8[*]ArcTan (inj_Q IR (1 / 182%Z))[+] (nring 10[*]ArcTan (inj_Q IR (1 / 5118%Z))[+] nring 5[*]ArcTan (inj_Q IR (1 / 6072%Z)))). repeat apply bin_op_wd_unfolded; try apply eq_reflexive. apply (inj_Q_nring IR 17). apply (inj_Q_nring IR 8). apply (inj_Q_nring IR 10). apply (inj_Q_nring IR 5). 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 CoRN.stdlib_omissions.Q