proposition: Lemma R_dist_opp_compat: forall x y, R_dist (- x) (- y) = R_dist x y.
proof: Proof. intros ; unfold R_dist ; rewrite Rminus_opp, Rabs_minus_sym ; apply Rabs_eq_compat ; ring. Qed.
imports: Reals Ranalysis_def Rinterval MyRIneq Lra