proposition: Lemma MVP_BernsteinNonNeg : forall m n i (H:(i <= n)%nat) v (a:Q), 0 <= a -> a <= 1 -> 0 <= @MVP_apply Q_as_CRing m ((Bernstein _ H)!(MVP_C_ _ _ a)) v.
proof: Proof. intros m n i H v a Ha0 Ha1. induction v. apply: BernsteinNonNeg; auto. simpl. replace RHS with (MVP_apply Q_as_CRing (Bernstein _ H) ! (MVP_C_ Q_as_CRing n0 a) v). apply IHv. apply: MVP_apply_wd; try reflexivity. rewrite -> BernsteinApplyRingHom. auto with *. 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