proposition: Lemma Rabs_le_between : forall x y, (Rabs x <= y <-> -y <= x <= y).
proof: Proof. split. split. rewrite <-(Ropp_involutive x). apply Ropp_le_contravar. apply (Rle_trans _ (Rabs x)). rewrite <-Rabs_Ropp. apply RRle_abs. apply H. apply (Rle_trans _ (Rabs x)). apply RRle_abs. apply H. intros. unfold Rabs. destruct (Rcase_abs x). rewrite <-(Ropp_involutive y). apply Ropp_le_contravar. apply H. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)