proposition: Lemma MVP_uc_fun_correct : forall n (p:MultivariatePolynomial Q_as_CRing n), MVP_uc_fun_correct_sig n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
proof: Proof. intros n p. generalize (fun e => MVP_uc_fun_close n e p). generalize (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)). clear p. induction n; intros a b H. apply ball_eq. intros. apply (H (exist _ _ H0)). intros x Hx0 Hx1. apply IHn. intros e. apply H; 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