proposition: Lemma Pi_Formula : (((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)))[=] Pi[/]FourNZ).
proof: Proof. assert (H0:-(1) <= (1/(23%Z)) <= 1). split; discriminate. assert (H1:-(1) <= (1/(182%Z)) <= 1). split; discriminate. assert (H2:-(1) <= (1/(5118%Z)) <= 1). split; discriminate. assert (H3:-(1) <= (1/(6072%Z)) <= 1). split; discriminate. set (y0:=(iter_nat 17 _ (f (1/23%Z)) 0)). set (y1:=(iter_nat 8 _ (f (1/182%Z)) 0)). set (y2:=(iter_nat 10 _ (f (1/5118%Z)) 0)). set (y3:=(iter_nat 5 _ (f (1/6072%Z)) 0)). rstepl (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)))). csetoid_replace ((nring 17)[*]ArcTan (inj_Q IR (1 / 23%Z))) (ArcTan (inj_Q IR y0)); [|apply (reflect_right (ArcTan_multiple H0 17)); vm_compute; constructor]. csetoid_replace ((nring 8)[*]ArcTan (inj_Q IR (1 / 182%Z))) (ArcTan (inj_Q IR y1)); [|apply (reflect_right (ArcTan_multiple H1 8)); vm_compute; constructor]. csetoid_replace ((nring 10)[*]ArcTan (inj_Q IR (1 / 5118%Z))) (ArcTan (inj_Q IR y2)); [|apply (reflect_right (ArcTan_multiple H2 10)); vm_compute; constructor]. csetoid_replace ((nring 5)[*]ArcTan (inj_Q IR (1 / 6072%Z))) (ArcTan (inj_Q IR y3)); [|apply (reflect_right (ArcTan_multiple H3 5)); vm_compute; constructor]. vm_compute in y0. vm_compute in y1. vm_compute in y2. vm_compute in y3. csetoid_replace (ArcTan (inj_Q IR y0)[+]ArcTan (inj_Q IR y1)) (ArcTan (inj_Q IR (f y0 y1))); [|apply ArcTan_plus_ArcTan_Q; try split; vm_compute; discriminate]. csetoid_replace (ArcTan (inj_Q IR y2)[+]ArcTan (inj_Q IR y3)) (ArcTan (inj_Q IR (f y2 y3))); [|apply ArcTan_plus_ArcTan_Q; try split; vm_compute; discriminate]. set (z0 := (f y0 y1)). set (z1 := (f y2 y3)). vm_compute in z0. vm_compute in z1. csetoid_replace (ArcTan (inj_Q IR z0)[+]ArcTan (inj_Q IR z1)) (ArcTan (inj_Q IR (f z0 z1))); [|apply ArcTan_plus_ArcTan_Q; try split; vm_compute; discriminate]. set (z3:= (f z0 z1)). vm_compute in z3. eapply eq_transitive;[|apply ArcTan_one]. apply ArcTan_wd. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). 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