proposition: Lemma MVP_map_C_ : forall R S (f:RingHom R S) n c, MVP_map f n (MVP_C_ _ _ c)[=]MVP_C_ _ _ (f c).
proof: Proof. induction n. intros c; reflexivity. intros c. simpl. change (cpoly_map (MVP_map f n) (_C_ (MVP_C_ R n c))[=]_C_ (MVP_C_ S n (f c))). rewrite -> cpoly_map_C. rewrite -> IHn. 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