proposition: Lemma MVP_is_Bound01_mult01 : forall n M p x, (0 <= x)%CR -> (x <= 1)%CR -> MVP_is_Bound01 n M p -> MVP_is_Bound01 n M (MVP_C_ CRasCRing n x[*]p).
proof: Proof. induction n; intros M p x Hx0 Hx1 H. simpl. change (msp_car CR) in p. eapply AbsSmall_leEq_trans;[|apply mult_resp_AbsSmall;[|apply H]]; auto. rewrite <- (CRmult_1_l M) at 2. apply mult_resp_leEq_rht; auto. simpl in H. unfold AbsSmall in H. rewrite <- CRabs_AbsSmall in H. eapply leEq_transitive;[|apply H]. apply CRabs_nonneg. simpl. intros y Hy0 Hy1. rewrite -> mult_apply. rewrite -> c_apply. apply IHn; auto. 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