proposition: Lemma Rabs_lt_between : forall x y, (Rabs x < y <-> -y < x < y).
proof: Proof. split. intros; split; now apply Rabs_def2. intros (H1,H2); now apply Rabs_def1. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)