proposition: Lemma Rabs_lt_between' : forall x y z, Rabs (x - y) < z <-> y-z < x < y+z.
proof: Proof. split ; intros. cut (-z < x-y < z). intros ; split. rewrite <- (Rplus_0_l x). rewrite <-(Rplus_opp_r y). rewrite Rplus_assoc. apply Rplus_lt_compat_l. rewrite Rplus_comm. apply H0. rewrite <- (Rplus_0_l x). rewrite <-(Rplus_opp_r y). rewrite Rplus_assoc. apply Rplus_lt_compat_l. rewrite Rplus_comm. apply H0. apply (Rabs_lt_between (x-y) z). apply H. apply (Rabs_lt_between (x-y) z). split. rewrite <- (Rplus_0_r (-z)). rewrite <-(Rplus_opp_r y). rewrite <- Rplus_assoc. apply Rplus_lt_compat_r. rewrite Rplus_comm. apply H. rewrite <- (Rplus_0_r z). rewrite <-(Rplus_opp_r y). rewrite <- Rplus_assoc. apply Rplus_lt_compat_r. rewrite Rplus_comm. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)