proposition: Lemma Rabs_lt_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 Rlt_le_trans with (2 := RmaxLess2 _ _). apply Ropp_lt_contravar, Hx. apply Rlt_le_trans with (2 := RmaxLess1 _ _). apply Hx. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)