fact: Definition r_pi (r:Q) : CR := ((scale (176%Z*r) (rational_arctan_small (widen_interval small_per_57)) + scale (28%Z*r) (rational_arctan_small (widen_interval small_per_239))) + (scale (-(48%Z)*r) (rational_arctan_small (widen_interval small_per_682)) + scale (96%Z*r) (rational_arctan_small (widen_interval small_per_12943))))%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 MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q