proposition: Lemma BernsteinApplyRingHom : forall R F (eta: RingHom R F) n i (H:(i <= n)%nat) a, (Bernstein F H) ! (eta a)[=](eta (Bernstein R H) ! a).
proof: Proof. induction n. simpl. intros _ _ a. do 2 rewrite -> one_apply. auto with *. intros [|i] H a; simpl;[|destruct (le_lt_eq_dec (S i) (S n) H)]; autorewrite with apply ringHomPush; repeat rewrite -> IHn; reflexivity. 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