proposition: Lemma MVP_uc_fun_sub_Q : forall n (p:MultivariatePolynomial _ (S n)) x, 0 <= x -> x <= 1 -> msp_eq (MVP_uc_fun (S n) p ('x)%CR) (MVP_uc_fun n (p!(MVP_C_ _ _ x))).
proof: Proof. intros n p x Hx0 Hx1. unfold MVP_uc_fun. apply: n_Cap_wd. intros e1 e2. simpl. unfold Cap_raw. simpl. rewrite Qplus_0_r. change (ball (proj1_sig e1 + proj1_sig e2) (MVP_uc_Q n p ! (MVP_C_ Q_as_CRing n (Qmax 0 (Qmin 1 x)))) (MVP_uc_Q n p ! (MVP_C_ Q_as_CRing n x))). rewrite -> Qle_min_r in Hx1. rewrite -> Hx1. rewrite -> Qle_max_r in Hx0. rewrite -> Hx0. apply ball_refl. apply (Qpos_nonneg (e1+e2)). 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