proposition: Lemma CRabs_scale (a : Q) (x : CR) : CRabs (scale a x) == scale (Qabs a) (CRabs x).
proof: Proof. apply lift_eq_complete with (f := uc_compose CRabs (scale a)) (g := uc_compose (scale (Qabs a)) CRabs). intros q e1 e2. rewrite Qplus_0_r. change (@ball Q_as_MetricSpace (proj1_sig e1 + proj1_sig e2) (Qabs (a * q)) (Qabs a * Qabs q)%Q). apply <- ball_eq_iff. apply Qball_0, Qabs_Qmult. apply (Qpos_ispos (e1+e2)). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability