proposition: Lemma Pi_Formula : (((nring 44)[*]ArcTan (inj_Q IR (1 / 57%Z))[-] (nring 12)[*]ArcTan (inj_Q IR (1 / 682%Z))[+] (nring 7)[*]ArcTan (inj_Q IR (1 / 239%Z))[+] (nring 24)[*]ArcTan (inj_Q IR (1 / 12943%Z)))[=] Pi[/]FourNZ).
proof: Proof. assert (H0:-(1) <= (1/(57%Z)) <= 1). split; discriminate. assert (H1:-(1) <= (1/(239%Z)) <= 1). split; discriminate. assert (H2:-(1) <= (1/(682%Z)) <= 1). split; discriminate. assert (H3:-(1) <= (1/(12943%Z)) <= 1). split; discriminate. set (y0:=(iter_nat 44 _ (f (1/57%Z)) 0)). set (y1:=(iter_nat 7 _ (f (1/239%Z)) 0)). set (y2:=(iter_nat 12 _ (f (1/682%Z)) 0)). set (y3:=(iter_nat 24 _ (f (1/12943%Z)) 0)). rstepl (nring 44[*]ArcTan (inj_Q IR (1 / 57%Z))[+] [--](nring 12[*]ArcTan (inj_Q IR (1 / 682%Z)))[+] (nring 7[*]ArcTan (inj_Q IR (1 / 239%Z))[+] nring 24[*]ArcTan (inj_Q IR (1 / 12943%Z)))). csetoid_replace ((nring 44)[*]ArcTan (inj_Q IR (1 / 57%Z))) (ArcTan (inj_Q IR y0)); [|apply: (reflect_right (ArcTan_multiple H0 44)); now vm_compute]. csetoid_replace ((nring 7)[*]ArcTan (inj_Q IR (1 / 239%Z))) (ArcTan (inj_Q IR y1)); [|apply: (reflect_right (ArcTan_multiple H1 7)); now vm_compute]. csetoid_replace ((nring 12)[*]ArcTan (inj_Q IR (1 / 682%Z))) (ArcTan (inj_Q IR y2)); [|apply: (reflect_right (ArcTan_multiple H2 12)); now vm_compute]. csetoid_replace ((nring 24)[*]ArcTan (inj_Q IR (1 / 12943%Z))) (ArcTan (inj_Q IR y3)); [|apply: (reflect_right (ArcTan_multiple H3 24)); now vm_compute]. vm_compute in y0. vm_compute in y1. vm_compute in y2. vm_compute in y3. csetoid_replace ([--](ArcTan (inj_Q IR y2))) (ArcTan (inj_Q IR (-y2))); [|csetoid_rewrite_rev (ArcTan_inv (inj_Q IR y2)); apply ArcTan_wd; apply eq_symmetric; apply (inj_Q_inv IR y2)]. csetoid_replace (ArcTan (inj_Q IR y0)[+]ArcTan (inj_Q IR (-y2))) (ArcTan (inj_Q IR (f y0 (-y2)))); [|apply ArcTan_plus_ArcTan_Q; try split; now vm_compute]. csetoid_replace (ArcTan (inj_Q IR y1)[+]ArcTan (inj_Q IR y3)) (ArcTan (inj_Q IR (f y1 y3))); [|apply ArcTan_plus_ArcTan_Q; try split; now vm_compute]. set (z0 := (f y0 (-y2))). set (z1 := (f y1 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; now vm_compute]. 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 MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q