proposition: Lemma MVP_uc_fun_correct_Q : forall n (p:MultivariatePolynomial Q_as_CRing n), MVP_uc_fun_correct_sig_Q n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
proof: Proof. induction n; intros p. change ('p=='p)%CR. reflexivity. intros x Hx0 Hx1. change (MVP_uc_fun_correct_sig_Q n (MVP_uc_fun (S n) p ('x)%CR) (MVP_CR_apply n ((MVP_map inject_Q_hom (S n) p)!(MVP_C_ CRasCRing _ ('x)%CR)))). eapply MVP_uc_fun_correct_sig_Q_wd;[apply MVP_uc_fun_sub_Q; auto| |apply IHn]. apply Morphism_prf. simpl. setoid_replace (MVP_C_ CRasCRing n (' x)%CR) with ((MVP_map inject_Q_hom n) (MVP_C_ Q_as_CRing n x)). symmetry. apply cpoly_map_apply. clear - n. induction n. reflexivity. simpl. refine (csf_wd _ _ _ _ _ _). apply IHn. 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