proposition: Lemma gball_CRmult_Q_nonneg (e a : Q) (x y : CR) : (0 <= a)%Q -> ball e x y -> ball (a * e) ('a * x) ('a * y).
proof: Proof. intros A1 A2. rewrite <- (Qabs_pos a) at 1; [apply gball_CRmult_Q |]; easy. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs