proposition: Lemma MVP_apply_hom_strext : forall (F:CRing) n (v:Vector.t F n), fun_strext (fun (p:MultivariatePolynomial F n) => MVP_apply _ p v).
proof: Proof. induction n. intros v x y. simpl. auto with *. intros v x y H. simpl in H. destruct (csbf_strext _ _ _ _ _ _ _ _ (IHn _ _ _ H)) as [H0 | H0]. assumption. elim (ap_irreflexive _ _ H0). Defined.
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