# Library Coqtail.mytheories.myReals.MyR_dist

Require Import Reals Ranalysis_def Rinterval.
Require Import MyRIneq Fourier.

Lemma R_dist_opp_compat: x y,
R_dist (- x) (- y) = R_dist x y.
Proof.
intros ; unfold R_dist ; rewrite Rminus_opp, Rabs_minus_sym ;
apply Rabs_eq_compat ; ring.
Qed.

Lemma R_dist_scal_compat: a x y,
R_dist (a × x) (a × y) = Rabs a × R_dist x y.
Proof.
intros ; unfold R_dist ; rewrite <- Rabs_mult ;
apply Rabs_eq_compat ; ring.
Qed.

Lemma R_dist_minus_compat : x y z, R_dist (x - z) (y - z) = R_dist x y.
Proof.
intros ; apply Rabs_eq_compat ; ring.
Qed.

Lemma R_dist_Rplus_compat: x h, R_dist (x + h) x = Rabs h.
Proof.
intros ; apply Rabs_eq_compat ; ring.
Qed.

Lemma R_dist_Rminus_compat: x h, R_dist (x - h) x = Rabs h.
Proof.
intros ; rewrite <- Rabs_Ropp ; apply Rabs_eq_compat ; ring.
Qed.

Lemma Rlt_le_Rdist_compat : a b c, a < bb cR_dist c b < R_dist c a.
Proof.
intros a b c aleb alec ; unfold R_dist ; do 3 (rewrite Rabs_right || fourier).
Qed.

Lemma Rle_lt_Rdist_compat : a b c, a bb < cR_dist b a < R_dist c a.
Proof.
intros a b c aleb alec ; unfold R_dist ; do 3 (rewrite Rabs_right || fourier).
Qed.