proposition: Lemma R_dist_scal_compat: forall a x y, R_dist (a * x) (a * y) = Rabs a * R_dist x y.
proof: Proof. intros ; unfold R_dist ; rewrite <- Rabs_mult ; apply Rabs_eq_compat ; ring. Qed.
imports: Reals Ranalysis_def Rinterval MyRIneq Lra