proposition: Lemma n_Function_ball01_mult_C : forall n (e:Qpos) c q1 q2, (0 <= c)%CR -> (c <= 1)%CR -> (n_Function_ball01 n (proj1_sig e) (MVP_CR_apply n q1) (MVP_CR_apply n q2)) -> (n_Function_ball01 n (proj1_sig e) (MVP_CR_apply n ((MVP_C_ CRasCRing _ c)[*]q1)) (MVP_CR_apply n ((MVP_C_ CRasCRing _ c)[*]q2))).
proof: Proof. induction n; intros e c q1 q2 Hc0 Hc1 H. change (ball (proj1_sig e) (c * q1)%CR (c * q2)%CR). rewrite <- CRAbsSmall_ball. change (@cg_minus CRasCOrdField (c * q1)%CR (c * q2)%CR) with (c*q1 - c*q2)%CR. setoid_replace (c*q1 - c*q2)%CR with (c * (q1 - q2))%CR by ring. apply AbsSmall_leEq_trans with (c * 'proj1_sig e)%CR. rewrite <- (CRmult_1_l ('proj1_sig e)%CR) at 2. apply mult_resp_leEq_rht; auto. simpl. apply CRle_Qle, Qpos_nonneg. apply mult_resp_AbsSmall; auto. apply (CRAbsSmall_ball q1 q2). exact H. intros x Hx0 Hx1. change (n_Function_ball01 n (proj1_sig e) (MVP_CR_apply _ (MVP_C_ CRasCRing _ c[*]q1) ! (MVP_C_ CRasCRing _ x)) (MVP_CR_apply _ (MVP_C_ CRasCRing _ c[*]q2) ! (MVP_C_ CRasCRing _ x))). eapply n_Function_ball01_wd. reflexivity. apply Morphism_prf. eapply eq_transitive. apply mult_apply. apply mult_wdl. simpl. apply c_apply. apply Morphism_prf. eapply eq_transitive. apply mult_apply. apply mult_wdl. simpl. apply c_apply. apply IHn; auto. 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