proposition: Lemma MVP_c_mult_apply: forall F n (p : MultivariatePolynomial F n) c v, MVP_apply F (MVP_C_ _ _ c[*]p) v[=]c[*]MVP_apply F p v.
proof: Proof. induction v. reflexivity. simpl. rewrite <- IHv. rewrite -> c_mult_apply. reflexivity. Qed.
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