proposition: Lemma Rabs_le_between_Rmax : forall x m M, m <= x <= M -> Rabs x <= Rmax M (-m).
proof: Proof. intros x m M Hx. unfold Rabs ; destruct Rcase_abs as [H|H]. apply Rle_trans with (2 := RmaxLess2 _ _). apply Ropp_le_contravar, Hx. apply Rle_trans with (2 := RmaxLess1 _ _). apply Hx. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)