proposition: Lemma sign_min_max (a b : R) : sign (b - a) * (Rmax a b - Rmin a b) = b - a.
proof: Proof. unfold sign. case total_order_T as [[H|H]|H]. assert (K := proj2 (Rminus_le_0 a b) (Rlt_le _ _ H)). rewrite (Rmax_right _ _ K) (Rmin_left _ _ K). apply Rmult_1_l. rewrite -H. apply Rmult_0_l. assert (K : b <= a). apply Rnot_lt_le. contradict H. apply Rle_not_lt. apply -> Rminus_le_0. now apply Rlt_le. rewrite (Rmax_left _ _ K) (Rmin_right _ _ K). ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)