fact: Fixpoint MVP_poor_Bound01 n : MultivariatePolynomial Q_as_CRing n -> Q := match n return MultivariatePolynomial Q_as_CRing n -> Q with | O => Qabs | S n' => fix MVP_poor_Bound01_H p : Q := match p with | cpoly_zero _ => 0 | cpoly_linear _ s p' => MVP_poor_Bound01 n' s + MVP_poor_Bound01_H p' end end.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg CoRN.algebra.RSetoid