proposition: Lemma MVP_CR_apply_prf : forall n (morph : MultivariatePolynomial CRasCRing n -> n_Function (msp_as_RSetoid CR) (msp_as_RSetoid CR) n) (morph_prf : forall x1 x2 : MultivariatePolynomial CRasCRing n, x1 [=] x2 -> morph x1 [=] morph x2) p (x y : CR), msp_eq x y -> st_eq (morph (p!(MVP_C_ CRasCRing n x))) (morph (p!(MVP_C_ CRasCRing n y))).
proof: Proof. intros. apply morph_prf. apply cpoly_apply_wd. reflexivity. apply csf_wd. apply H. 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 CoRN.algebra.RSetoid