fact: Definition r_pi (r:Q) : CR := ((scale (68%Z*r) (rational_arctan_small (widen_interval small_per_23)) + scale (32%Z*r) (rational_arctan_small (widen_interval small_per_182))) + (scale (40%Z*r) (rational_arctan_small (widen_interval small_per_5118)) + scale (20%Z*r) (rational_arctan_small (widen_interval small_per_6072))))%CR.
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