proposition: Lemma gball_CRmult_Q (e a : Q) (x y : CR) : ball e x y -> ball (Qabs a * e) ('a * x) ('a * y).
proof: Proof. intro A. apply gball_CRabs. setoid_replace ('a * x - 'a * y) with ('a * (x - y)) by (unfold canonical_names.equiv, msp_Equiv; ring). rewrite CRabs_CRmult_Q, <- CRmult_Qmult. assert (0 <= 'Qabs a) by (apply CRle_Qle, Qabs_nonneg). apply (orders.order_preserving (CRmult (' Qabs a))). now apply gball_CRabs. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs