General theory of min and max, and use in ssrnum

- min and max can now be used in a partial order (sometimes under preconditions)
- min and max can now be used in a numDomainType (sometimes under preconditions)

4 files changed, 572 insertions, 187 deletions

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 3ed2825..950546b 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -210,19 +210,19 @@ Proof. by case: b; apply lter_distl. Qed.
 
 Lemma lersif_minr :
   (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b).
-Proof. by case: b; rewrite /= ltexI. Qed.
+Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed.
 
 Lemma lersif_minl :
   (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b).
-Proof. by case: b; rewrite /= lteIx. Qed.
+Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed.
 
 Lemma lersif_maxr :
   (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b).
-Proof. by case: b; rewrite /= ltexU. Qed.
+Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed.
 
 Lemma lersif_maxl :
   (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b).
-Proof. by case: b; rewrite /= lteUx. Qed.
+Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed.
 
 End LersifOrdered.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 95c40cd..6dbfaf7 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -389,10 +389,10 @@ Notation "@ 'lerif' R" := (@Order.leif ring_display R)
 Notation comparabler := (@Order.comparable ring_display _) (only parsing).
 Notation "@ 'comparabler' R" := (@Order.comparable ring_display R)
   (at level 10, R at level 8, only parsing) : fun_scope.
-Notation maxr := (@Order.join ring_display _).
+Notation maxr := (@Order.max ring_display _).
 Notation "@ 'maxr' R" := (@Order.join ring_display R)
     (at level 10, R at level 8, only parsing) : fun_scope.
-Notation minr := (@Order.meet ring_display _).
+Notation minr := (@Order.min ring_display _).
 Notation "@ 'minr' R" := (@Order.meet ring_display R)
   (at level 10, R at level 8, only parsing) : fun_scope.
 
@@ -1550,6 +1550,8 @@ Definition subr_cp0 := (subr_lte0, subr_gte0).
 
 (* Comparability in a numDomain *)
 
+Lemma comparable0r x : (0 >=< x)%R = (x \is Num.real). Proof. by []. Qed.
+
 Lemma comparabler0 x : (x >=< 0)%R = (x \is Num.real).
 Proof. by rewrite comparable_sym. Qed.
 
@@ -1676,11 +1678,7 @@ Lemma ler_leVge x y : x <= 0 -> y <= 0 -> (x <= y) || (y <= x).
 Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) h /h; rewrite !ler_opp2. Qed.
 
 Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x).
-Proof.
-rewrite !realE; have [x_ge0 _|x_nge0 /= x_le0] := boolP (_ <= _); last first.
-  by have [/(le_trans x_le0)->|_ /(ler_leVge x_le0) //] := boolP (0 <= _).
-by have [/(ger_leVge x_ge0)|_ /le_trans->] := boolP (0 <= _); rewrite ?orbT.
-Qed.
+Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed.
 
 Lemma real_comparable x y : x \is real -> y \is real -> x >=< y.
 Proof. exact: real_leVge. Qed.
@@ -1699,35 +1697,37 @@ Proof. exact: rpredD. Qed.
 
 (* dichotomy and trichotomy *)
 
-Variant ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set :=
-  | LerNotGt of x <= y : ler_xor_gt x y (y - x) (y - x) true false
-  | GtrNotLe of y < x  : ler_xor_gt x y (x - y) (x - y) false true.
+Variant ler_xor_gt (x y : R) : R -> R -> R -> R -> R -> R ->
+    bool -> bool -> Set :=
+  | LerNotGt of x <= y : ler_xor_gt x y x x y y (y - x) (y - x) true false
+  | GtrNotLe of y < x  : ler_xor_gt x y y y x x (x - y) (x - y) false true.
 
-Variant ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set :=
-  | LtrNotGe of x < y  : ltr_xor_ge x y (y - x) (y - x) false true
-  | GerNotLt of y <= x : ltr_xor_ge x y (x - y) (x - y) true false.
+Variant ltr_xor_ge (x y : R) : R -> R -> R -> R -> R -> R ->
+    bool -> bool -> Set :=
+  | LtrNotGe of x < y  : ltr_xor_ge x y x x y y (y - x) (y - x) false true
+  | GerNotLt of y <= x : ltr_xor_ge x y y y x x (x - y) (x - y) true false.
 
-Variant comparer x y : R -> R ->
-  bool -> bool -> bool -> bool -> bool -> bool -> Set :=
-  | ComparerLt of x < y : comparer x y (y - x) (y - x)
+Variant comparer x y : R -> R -> R -> R -> R -> R ->
+    bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | ComparerLt of x < y : comparer x y x x y y (y - x) (y - x)
     false false false true false true
-  | ComparerGt of x > y : comparer x y (x - y) (x - y)
+  | ComparerGt of x > y : comparer x y y y x x (x - y) (x - y)
     false false true false true false
-  | ComparerEq of x = y : comparer x y 0 0
+  | ComparerEq of x = y : comparer x y x x x x 0 0
     true true true true false false.
 
-Lemma real_leP x y :
-    x \is real -> y \is real ->
-  ler_xor_gt x y `|x - y| `|y - x| (x <= y) (y < x).
+Lemma real_leP x y : x \is real -> y \is real ->
+  ler_xor_gt x y (min y x) (min x y) (max y x) (max x y)
+                 `|x - y| `|y - x| (x <= y) (y < x).
 Proof.
 move=> xR yR; case: (comparable_leP (real_leVge xR yR)) => xy.
 - by rewrite [`|x - y|]distrC !ger0_norm ?subr_cp0 //; constructor.
 - by rewrite [`|y - x|]distrC !gtr0_norm ?subr_cp0 //; constructor.
 Qed.
 
-Lemma real_ltP x y :
-    x \is real -> y \is real ->
-  ltr_xor_ge x y `|x - y| `|y - x| (y <= x) (x < y).
+Lemma real_ltP x y : x \is real -> y \is real ->
+  ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y)
+             `|x - y| `|y - x| (y <= x) (x < y).
 Proof. by move=> xR yR; case: real_leP=> //; constructor. Qed.
 
 Lemma real_ltNge : {in real &, forall x y, (x < y) = ~~ (y <= x)}.
@@ -1737,46 +1737,52 @@ Lemma real_leNgt : {in real &, forall x y, (x <= y) = ~~ (y < x)}.
 Proof. by move=> x y xR yR /=; case: real_leP. Qed.
 
 Lemma real_ltgtP x y : x \is real -> y \is real ->
-  comparer x y `|x - y| `|y - x|
-                (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
+  comparer x y (min y x) (min x y) (max y x) (max x y) `|x - y| `|y - x|
+               (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
 Proof.
-move=> xR yR; case: (comparable_ltgtP (real_leVge xR yR)) => [?|?|->].
-- by rewrite [`|x - y|]distrC !gtr0_norm ?subr_gt0//; constructor.
+move=> xR yR; case: (comparable_ltgtP (real_leVge yR xR)) => [?|?|->].
 - by rewrite [`|y - x|]distrC !gtr0_norm ?subr_gt0//; constructor.
+- by rewrite [`|x - y|]distrC !gtr0_norm ?subr_gt0//; constructor.
 - by rewrite subrr normr0; constructor.
 Qed.
 
-Variant ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set :=
-  | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x x false true
-  | Ltr0NotGe0 of x < 0  : ger0_xor_lt0 x (- x) true false.
+Variant ger0_xor_lt0 (x : R) : R -> R -> R -> R -> R ->
+    bool -> bool -> Set :=
+  | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x 0 0 x x x false true
+  | Ltr0NotGe0 of x < 0  : ger0_xor_lt0 x x x 0 0 (- x) true false.
 
-Variant ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set :=
-  | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x (- x) false true
-  | Gtr0NotGt0 of 0 < x  : ler0_xor_gt0 x x true false.
+Variant ler0_xor_gt0 (x : R) : R -> R -> R -> R -> R ->
+   bool -> bool -> Set :=
+  | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x x x 0 0 (- x) false true
+  | Gtr0NotGt0 of 0 < x  : ler0_xor_gt0 x 0 0 x x x true false.
 
-Variant comparer0 x :
-               R -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
-  | ComparerGt0 of 0 < x : comparer0 x x false false false true false true
-  | ComparerLt0 of x < 0 : comparer0 x (- x) false false true false true false
-  | ComparerEq0 of x = 0 : comparer0 x 0 true true true true false false.
+Variant comparer0 x : R -> R -> R -> R -> R ->
+    bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | ComparerGt0 of 0 < x : comparer0 x 0 0 x x x false false false true false true
+  | ComparerLt0 of x < 0 : comparer0 x x x 0 0 (- x) false false true false true false
+  | ComparerEq0 of x = 0 : comparer0 x 0 0 0 0 0 true true true true false false.
 
-Lemma real_ge0P x : x \is real -> ger0_xor_lt0 x `|x| (x < 0) (0 <= x).
+Lemma real_ge0P x : x \is real -> ger0_xor_lt0 x
+   (min 0 x) (min x 0) (max 0 x) (max x 0)
+  `|x| (x < 0) (0 <= x).
 Proof.
-move=> hx; rewrite -{2}[x]subr0; case: real_ltP;
+move=> hx; rewrite -[X in `|X|]subr0; case: real_leP;
 by rewrite ?subr0 ?sub0r //; constructor.
 Qed.
 
-Lemma real_le0P x : x \is real -> ler0_xor_gt0 x `|x| (0 < x) (x <= 0).
+Lemma real_le0P x : x \is real -> ler0_xor_gt0 x
+  (min 0 x) (min x 0) (max 0 x) (max x 0)
+  `|x| (0 < x) (x <= 0).
 Proof.
-move=> hx; rewrite -{2}[x]subr0; case: real_ltP;
+move=> hx; rewrite -[X in `|X|]subr0; case: real_ltP;
 by rewrite ?subr0 ?sub0r //; constructor.
 Qed.
 
-Lemma real_ltgt0P x :
-     x \is real ->
-  comparer0 x `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0).
+Lemma real_ltgt0P x : x \is real ->
+  comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0)
+            `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0).
 Proof.
-move=> hx; rewrite -{2}[x]subr0; case: real_ltgtP;
+move=> hx; rewrite -[X in `|X|]subr0; case: (@real_ltgtP 0 x);
 by rewrite ?subr0 ?sub0r //; constructor.
 Qed.
 
@@ -2766,6 +2772,111 @@ Proof. by rewrite -invr_gt1 ?invr_gt0 ?unitrV // invrK. Qed.
 Definition invr_lte1 := (invr_le1, invr_lt1).
 Definition invr_cp1 := (invr_gte1, invr_lte1).
 
+(* max and min *)
+
+Lemma addr_min_max x y : min x y + max x y = x + y.
+Proof. by rewrite /min /max; case: ifP => //; rewrite addrC. Qed.
+
+Lemma addr_max_min x y : max x y + min x y = x + y.
+Proof. by rewrite addrC addr_min_max. Qed.
+
+Lemma minr_to_max x y : min x y = x + y - max x y.
+Proof. by rewrite -[x + y]addr_min_max addrK. Qed.
+
+Lemma maxr_to_min x y : max x y = x + y - min x y.
+Proof. by rewrite -[x + y]addr_max_min addrK. Qed.
+
+Lemma real_oppr_max : {in real &, {morph -%R : x y / max x y >-> min x y : R}}.
+Proof.
+move=> x y x_real y_real; rewrite !(fun_if, if_arg) ltr_opp2.
+by case: real_ltgtP => // ->.
+Qed.
+
+Lemma real_oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}.
+Proof.
+by move=> x y xr yr; rewrite -[RHS]opprK real_oppr_max ?realN// !opprK.
+Qed.
+
+Lemma real_addr_minl : {in real & real & real, @left_distributive R R +%R min}.
+Proof.
+by move=> x y z xr yr zr; case: (@real_leP (_ + _)); rewrite ?realD//;
+   rewrite lter_add2; case: real_leP.
+Qed.
+
+Lemma real_addr_minr : {in real & real & real, @right_distributive R R +%R min}.
+Proof. by move=> x y z xr yr zr; rewrite !(addrC x) real_addr_minl. Qed.
+
+Lemma real_addr_maxl : {in real & real & real, @left_distributive R R +%R max}.
+Proof.
+by move=> x y z xr yr zr; case: (@real_leP (_ + _)); rewrite ?realD//;
+   rewrite lter_add2; case: real_leP.
+Qed.
+
+Lemma real_addr_maxr : {in real & real & real, @right_distributive R R +%R max}.
+Proof. by move=> x y z xr yr zr; rewrite !(addrC x) real_addr_maxl. Qed.
+
+Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z).
+Proof.
+have [|x_gt0||->]// := comparableP x; last by rewrite !mul0r minxx.
+by rewrite !(fun_if, if_arg) lter_pmul2l//; case: (y < z).
+Qed.
+
+Lemma maxr_pmulr x y z : 0 <= x -> x * max y z = max (x * y) (x * z).
+Proof.
+have [|x_gt0||->]// := comparableP x; last by rewrite !mul0r maxxx.
+by rewrite !(fun_if, if_arg) lter_pmul2l//; case: (y < z).
+Qed.
+
+Lemma real_maxr_nmulr x y z : x <= 0 -> y \is real -> z \is real ->
+  x * max y z = min (x * y) (x * z).
+Proof.
+move=> x0 yr zr; rewrite -[_ * _]opprK -mulrN real_oppr_max// -mulNr.
+by rewrite minr_pmulr ?oppr_ge0// !(mulNr, mulrN, opprK).
+Qed.
+
+Lemma real_minr_nmulr x y z :  x <= 0 -> y \is real -> z \is real ->
+  x * min y z = max (x * y) (x * z).
+Proof.
+move=> x0 yr zr; rewrite -[_ * _]opprK -mulrN real_oppr_min// -mulNr.
+by rewrite maxr_pmulr ?oppr_ge0// !(mulNr, mulrN, opprK).
+Qed.
+
+Lemma minr_pmull x y z : 0 <= x -> min y z * x = min (y * x) (z * x).
+Proof. by move=> *; rewrite mulrC minr_pmulr // ![_ * x]mulrC. Qed.
+
+Lemma maxr_pmull x y z : 0 <= x -> max y z * x = max (y * x) (z * x).
+Proof. by move=> *; rewrite mulrC maxr_pmulr // ![_ * x]mulrC. Qed.
+
+Lemma real_minr_nmull x y z : x <= 0 -> y \is real -> z \is real ->
+  min y z * x = max (y * x) (z * x).
+Proof. by move=> *; rewrite mulrC real_minr_nmulr // ![_ * x]mulrC. Qed.
+
+Lemma real_maxr_nmull x y z : x <= 0 -> y \is real -> z \is real ->
+  max y z * x = min (y * x) (z * x).
+Proof. by move=> *; rewrite mulrC real_maxr_nmulr // ![_ * x]mulrC. Qed.
+
+Lemma real_maxrN x : x \is real -> max x (- x) = `|x|.
+Proof.
+move=> x_real; rewrite /max.
+by case: real_ge0P => // [/ge0_cp [] | /lt0_cp []];
+   case: (@real_leP (- x) x); rewrite ?realN.
+Qed.
+
+Lemma real_maxNr x : x \is real -> max (- x) x = `|x|.
+Proof.
+by move=> x_real; rewrite comparable_maxC ?real_maxrN ?real_comparable ?realN.
+Qed.
+
+Lemma real_minrN x : x \is real -> min x (- x) = - `|x|.
+Proof.
+by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxNr ?realN.
+Qed.
+
+Lemma real_minNr x : x \is real ->  min (- x) x = - `|x|.
+Proof.
+by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxrN ?realN.
+Qed.
+
 (* norm *)
 
 Lemma real_ler_norm x : x \is real -> x <= `|x|.
@@ -3594,25 +3705,30 @@ Implicit Types x y z t : R.
 Lemma num_real x : x \is real. Proof. exact: num_real. Qed.
 Hint Resolve num_real : core.
 
-Lemma lerP x y : ler_xor_gt x y `|x - y| `|y - x| (x <= y) (y < x).
+Lemma lerP x y : ler_xor_gt x y (min y x) (min x y) (max y x) (max x y)
+                                `|x - y| `|y - x| (x <= y) (y < x).
 Proof. exact: real_leP. Qed.
 
-Lemma ltrP x y : ltr_xor_ge x y `|x - y| `|y - x| (y <= x) (x < y).
+Lemma ltrP x y : ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y)
+                                `|x - y| `|y - x| (y <= x) (x < y).
 Proof. exact: real_ltP. Qed.
 
 Lemma ltrgtP x y :
-   comparer x y `|x - y| `|y - x| (y == x) (x == y)
+   comparer x y  (min y x) (min x y) (max y x) (max x y)
+                 `|x - y| `|y - x| (y == x) (x == y)
                  (x >= y) (x <= y) (x > y) (x < y) .
 Proof. exact: real_ltgtP. Qed.
 
-Lemma ger0P x : ger0_xor_lt0 x `|x| (x < 0) (0 <= x).
+Lemma ger0P x : ger0_xor_lt0 x (min 0 x) (min x 0) (max 0 x) (max x 0)
+                                `|x| (x < 0) (0 <= x).
 Proof. exact: real_ge0P. Qed.
 
-Lemma ler0P x : ler0_xor_gt0 x `|x| (0 < x) (x <= 0).
+Lemma ler0P x : ler0_xor_gt0 x (min 0 x) (min x 0) (max 0 x) (max x 0)
+                                `|x| (0 < x) (x <= 0).
 Proof. exact: real_le0P. Qed.
 
-Lemma ltrgt0P x :
-  comparer0 x `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0).
+Lemma ltrgt0P x : comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0)
+  `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0).
 Proof. exact: real_ltgt0P. Qed.
 
 (* sign *)
@@ -3862,93 +3978,40 @@ Proof. exact: real_leif_AGM2_scaled. Qed.
 
 Section MinMax.
 
-(* GG: Many of the first lemmas hold unconditionally, and others hold for    *)
-(* the real subset of a general domain.                                      *)
-
-Lemma addr_min_max x y : min x y + max x y = x + y.
-Proof.
-case: (lerP x y)=> [| /ltW] hxy;
-  first by rewrite (meet_idPl hxy) (join_idPl hxy).
-by rewrite (meet_idPr hxy) (join_idPr hxy) addrC.
-Qed.
-
-Lemma addr_max_min x y : max x y + min x y = x + y.
-Proof. by rewrite addrC addr_min_max. Qed.
-
-Lemma minr_to_max x y : min x y = x + y - max x y.
-Proof. by rewrite -[x + y]addr_min_max addrK. Qed.
-
-Lemma maxr_to_min x y : max x y = x + y - min x y.
-Proof. by rewrite -[x + y]addr_max_min addrK. Qed.
-
 Lemma oppr_max : {morph -%R : x y / max x y >-> min x y : R}.
-Proof.
-by move=> x y; case: leP; rewrite -lter_opp2 => hxy;
-  rewrite ?(meet_idPr hxy) ?(meet_idPl (ltW hxy)).
-Qed.
+Proof. by move=> x y; apply: real_oppr_max. Qed.
 
-Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}.
-Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed.
+Lemma oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}.
+Proof. by move=> x y; apply: real_oppr_min. Qed.
 
 Lemma addr_minl : @left_distributive R R +%R min.
-Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
+Proof. by move=> x y z; apply: real_addr_minl. Qed.
 
 Lemma addr_minr : @right_distributive R R +%R min.
-Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed.
+Proof. by move=> x y z; apply: real_addr_minr. Qed.
 
 Lemma addr_maxl : @left_distributive R R +%R max.
-Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
+Proof. by move=> x y z; apply: real_addr_maxl. Qed.
 
 Lemma addr_maxr : @right_distributive R R +%R max.
-Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
-
-Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z).
-Proof.
-case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx.
-by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP.
-Qed.
+Proof. by move=> x y z; apply: real_addr_maxr. Qed.
 
 Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z).
-Proof.
-move=> hx; rewrite -[_ * _]opprK -mulNr minr_pmulr ?oppr_cp0 //.
-by rewrite oppr_min !mulNr !opprK.
-Qed.
-
-Lemma maxr_pmulr x y z : 0 <= x -> x * max y z = max (x * y) (x * z).
-Proof.
-move=> hx; rewrite -[_ * _]opprK -mulrN oppr_max minr_pmulr //.
-by rewrite oppr_min !mulrN !opprK.
-Qed.
+Proof. by move=> x_le0; apply: real_minr_nmulr. Qed.
 
 Lemma maxr_nmulr x y z : x <= 0 -> x * max y z = min (x * y) (x * z).
-Proof.
-move=> hx; rewrite -[_ * _]opprK -mulrN oppr_max minr_nmulr //.
-by rewrite oppr_max !mulrN !opprK.
-Qed.
-
-Lemma minr_pmull x y z : 0 <= x -> min y z * x = min (y * x) (z * x).
-Proof. by move=> *; rewrite mulrC minr_pmulr // ![_ * x]mulrC. Qed.
+Proof. by move=> x_le0; apply: real_maxr_nmulr. Qed.
 
 Lemma minr_nmull x y z : x <= 0 -> min y z * x = max (y * x) (z * x).
-Proof. by move=> *; rewrite mulrC minr_nmulr // ![_ * x]mulrC. Qed.
-
-Lemma maxr_pmull x y z : 0 <= x -> max y z * x = max (y * x) (z * x).
-Proof. by move=> *; rewrite mulrC maxr_pmulr // ![_ * x]mulrC. Qed.
+Proof. by move=> x_le0; apply: real_minr_nmull. Qed.
 
 Lemma maxr_nmull x y z : x <= 0 -> max y z * x = min (y * x) (z * x).
-Proof. by move=> *; rewrite mulrC maxr_nmulr // ![_ * x]mulrC. Qed.
-
-Lemma maxrN x : max x (- x) = `|x|.
-Proof. by case: ger0P=> [/ge0_cp [] | /lt0_cp []]; case: (leP (- x) x). Qed.
+Proof. by move=> x_le0; apply: real_maxr_nmull. Qed.
 
-Lemma maxNr x : max (- x) x = `|x|.
-Proof. by rewrite joinC maxrN. Qed.
-
-Lemma minrN x : min x (- x) = - `|x|.
-Proof. by rewrite -[min _ _]opprK oppr_min opprK maxNr. Qed.
-
-Lemma minNr x : min (- x) x = - `|x|.
-Proof. by rewrite -[min _ _]opprK oppr_min opprK maxrN. Qed.
+Lemma maxrN x : max x (- x) = `|x|.   Proof. exact: real_maxrN. Qed.
+Lemma maxNr x : max (- x) x = `|x|.   Proof. exact: real_maxNr. Qed.
+Lemma minrN x : min x (- x) = - `|x|. Proof. exact: real_minrN. Qed.
+Lemma minNr x : min (- x) x = - `|x|. Proof. exact: real_minNr. Qed.
 
 End MinMax.
 
@@ -3959,7 +4022,7 @@ Variable p : {poly R}.
 Lemma poly_itv_bound a b : {ub | forall x, a <= x <= b -> `|p.[x]| <= ub}.
 Proof.
 have [ub le_p_ub] := poly_disk_bound p (Num.max `|a| `|b|).
-exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // lexU !ler_normr.
+exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // le_maxr !ler_normr.
 by have [_|_] := ler0P x; rewrite ?ler_opp2 ?le_a_x ?le_x_b orbT.
 Qed.
 
@@ -5231,7 +5294,11 @@ Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x.
 Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x.
 Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0,
                       normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN).
+Definition minr x y := if x <= y then x else y.
+Definition maxr x y := if x <= y then y else x.
 End NumIntegralDomainTheory.
+Arguments minr {_}.
+Arguments maxr {_}.
 
 Section NumIntegralDomainMonotonyTheory.
 Variables R R' : numDomainType.
@@ -5543,52 +5610,87 @@ Section RealDomainOperations.
 Variable R : realDomainType.
 Implicit Types x y z : R.
 Section MinMax.
-Definition minrC : @commutative R R min := @meetC _ R.
-Definition minrr : @idempotent R min := @meetxx _ R.
-Definition minr_l x y : x <= y -> min x y = x := @meet_l _ _ x y.
-Definition minr_r x y : y <= x -> min x y = y := @meet_r _ _ x y.
-Definition maxrC : @commutative R R max := @joinC _ R.
-Definition maxrr : @idempotent R max := @joinxx _ R.
-Definition maxr_l x y : y <= x -> max x y = x := @join_l _ _ x y.
-Definition maxr_r x y : x <= y -> max x y = y := @join_r _ _ x y.
-Definition minrA x y z : min x (min y z) = min (min x y) z := meetA x y z.
-Definition minrCA : @left_commutative R R min := meetCA.
-Definition minrAC : @right_commutative R R min := meetAC.
-Definition maxrA x y z : max x (max y z) = max (max x y) z := joinA x y z.
-Definition maxrCA : @left_commutative R R max := joinCA.
-Definition maxrAC : @right_commutative R R max := joinAC.
-Definition eqr_minl x y : (min x y == x) = (x <= y) := eq_meetl x y.
-Definition eqr_minr x y : (min x y == y) = (y <= x) := eq_meetr x y.
-Definition eqr_maxl x y : (max x y == x) = (y <= x) := eq_joinl x y.
-Definition eqr_maxr x y : (max x y == y) = (x <= y) := eq_joinr x y.
-Definition ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z) := lexI x y z.
-Definition ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x) := leIx x y z.
-Definition ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z) := lexU x y z.
-Definition ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x) := leUx y z x.
-Definition ltr_minr x y z : (x < min y z) = (x < y) && (x < z) := ltxI x y z.
-Definition ltr_minl x y z : (min y z < x) = (y < x) || (z < x) := ltIx x y z.
-Definition ltr_maxr x y z : (x < max y z) = (x < y) || (x < z) := ltxU x y z.
-Definition ltr_maxl x y z : (max y z < x) = (y < x) && (z < x) := ltUx x y z.
+
+Let mrE x y : ((minr x y = min x y) * (maxr x y = max x y))%type.
+Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed.
+Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?].
+Ltac mexact x := by mapply x.
+
+Local Notation min := minr.
+Local Notation max := maxr.
+
+Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed.
+Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed.
+Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed.
+Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed.
+Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed.
+Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed.
+Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed.
+
+Lemma minrA x y z : min x (min y z) = min (min x y) z.
+Proof. mexact @minA. Qed.
+
+Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed.
+Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed.
+Lemma maxrA x y z : max x (max y z) = max (max x y) z.
+Proof. mexact @maxA. Qed.
+
+Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed.
+Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed.
+Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed.
+Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed.
+Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed.
+Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed.
+
+Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z).
+Proof. mexact @le_minr. Qed.
+
+Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x).
+Proof. mexact @le_minl. Qed.
+
+Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z).
+Proof. mexact @le_maxr. Qed.
+
+Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x).
+Proof. mexact @le_maxl. Qed.
+
+Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z).
+Proof. mexact @lt_minr. Qed.
+
+Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x).
+Proof. mexact @lt_minl. Qed.
+
+Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z).
+Proof. mexact @lt_maxr. Qed.
+
+Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x).
+Proof. mexact @lt_maxl. Qed.
+
 Definition lter_minr := (ler_minr, ltr_minr).
 Definition lter_minl := (ler_minl, ltr_minl).
 Definition lter_maxr := (ler_maxr, ltr_maxr).
 Definition lter_maxl := (ler_maxl, ltr_maxl).
-Definition minrK x y : max (min x y) x = x := meetUKC y x.
-Definition minKr x y : min y (max x y) = y := joinKIC x y.
-Definition maxr_minl : @left_distributive R R max min := @joinIl _ R.
-Definition maxr_minr : @right_distributive R R max min := @joinIr _ R.
-Definition minr_maxl : @left_distributive R R min max := @meetUl _ R.
-Definition minr_maxr : @right_distributive R R min max := @meetUr _ R.
+
+Lemma minrK x y : max (min x y) x = x. Proof. mexact @minxK. Qed.
+Lemma minKr x y : min y (max x y) = y. Proof. mexact @maxKx. Qed.
+
+Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed.
+Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed.
+Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed.
+Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed.
+
 Variant minr_spec x y : bool -> bool -> R -> Type :=
 | Minr_r of x <= y : minr_spec x y true false x
 | Minr_l of y < x : minr_spec x y false true y.
 Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y).
-Proof. by case: leP; constructor. Qed.
+Proof. by rewrite mrE; case: leP; constructor. Qed.
+
 Variant maxr_spec x y : bool -> bool -> R -> Type :=
 | Maxr_r of y <= x : maxr_spec x y true false x
 | Maxr_l of x < y : maxr_spec x y false true y.
 Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y).
-Proof. by case: (leP y); constructor. Qed.
+Proof. by rewrite mrE; case: (leP y); constructor. Qed.
+
 End MinMax.
 End RealDomainOperations.
 
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 0a759e8..d8ad524 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -505,8 +505,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
     have /(find_root r.1)[n ub_rp] := xab0; exists n.
     have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}.
       have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2.
-      exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite ltxU ltr01.
-      by rewrite lexU orbC vM.
+      exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite lt_maxr ltr01.
+      by rewrite le_maxr orbC vM.
     exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n.
     rewrite ltr_pdivr_mulr // -(ltr_add2l h2) -mulr2n -mulr_natl divff //.
     rewrite -normr1 -(hornerC 1 a) -[1%:P]r_pq_1 hornerD.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 128396f..d8bcff1 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1076,6 +1076,7 @@ Arguments ge {_ _}.
 Arguments gt {_ _}.
 Arguments min {_ _}.
 Arguments max {_ _}.
+Arguments comparable {_ _}.
 
 Module Import POSyntax.
 
@@ -2654,7 +2655,7 @@ Context {disp : unit}.
 Local Notation porderType := (porderType disp).
 Context {T : porderType}.
 
-Implicit Types x y : T.
+Implicit Types (x y : T) (s : seq T).
 
 Lemma geE x y : ge x y = (y <= x). Proof. by []. Qed.
 Lemma gtE x y : gt x y = (y < x). Proof. by []. Qed.
@@ -2752,8 +2753,7 @@ Proof. by rewrite andbC lt_le_asym. Qed.
 
 Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym).
 
-Lemma lt_sorted_uniq_le (s : seq T) :
-   sorted lt s = uniq s && sorted le s.
+Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s.
 Proof.
 case: s => //= n s; elim: s n => //= m s IHs n.
 rewrite inE lt_neqAle negb_or IHs -!andbA.
@@ -2762,12 +2762,11 @@ rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm.
 by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)).
 Qed.
 
-Lemma eq_sorted_lt (s1 s2 : seq T) :
-  sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2.
+Lemma eq_sorted_lt s1 s2 : sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2.
 Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed.
 
-Lemma eq_sorted_le (s1 s2 : seq T) :
-   sorted le s1 -> sorted le s2 -> perm_eq s1 s2 -> s1 = s2.
+Lemma eq_sorted_le s1 s2 : sorted le s1 -> sorted le s2 ->
+  perm_eq s1 s2 -> s1 = s2.
 Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed.
 
 Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x).
@@ -2879,6 +2878,220 @@ Proof. by move=> /leifP; case: C comparableP => [] []. Qed.
 Lemma eqTleif x y C : x <= y ?= iff C -> C -> x = y.
 Proof. by move=> /eq_leif<-/eqP. Qed.
 
+(* min and max *)
+
+Lemma min_l x y : x <= y -> min x y = x. Proof. by case: comparableP. Qed.
+Lemma min_r x y : y <= x -> min x y = y. Proof. by case: comparableP. Qed.
+Lemma max_l x y : y <= x -> max x y = x. Proof. by case: comparableP. Qed.
+Lemma max_r x y : x <= y -> max x y = y. Proof. by case: comparableP. Qed.
+
+Lemma minxx : idempotent (min : T -> T -> T).
+Proof. by rewrite /min => x; rewrite ltxx. Qed.
+
+Lemma maxxx : idempotent (max : T -> T -> T).
+Proof. by rewrite /max => x; rewrite ltxx. Qed.
+
+Lemma eq_minl x y : (min x y == x) = (x <= y).
+Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed.
+
+Lemma eq_maxr x y : (max x y == y) = (x <= y).
+Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed.
+
+Lemma comparable_minl x y z : x >=< z -> y >=< z -> min x y >=< z.
+Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed.
+
+Lemma comparable_minr x y z : z >=< x -> z >=< y -> z >=< min x y.
+Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed.
+
+Lemma comparable_maxl x y z : x >=< z -> y >=< z -> max x y >=< z.
+Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed.
+
+Lemma comparable_maxr x y z : z >=< x -> z >=< y -> z >=< max x y.
+Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed.
+
+Section Comparable2.
+Variables (z x y : T) (cmp_xy : x >=< y).
+
+Lemma comparable_minC : min x y = min y x.
+Proof. by case: comparableP cmp_xy. Qed.
+
+Lemma comparable_maxC : max x y = max y x.
+Proof. by case: comparableP cmp_xy. Qed.
+
+Lemma comparable_eq_minr : (min x y == y) = (y <= x).
+Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed.
+
+Lemma comparable_eq_maxl : (max x y == x) = (y <= x).
+Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed.
+
+Lemma comparable_le_minr : (z <= min x y) = (z <= x) && (z <= y).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC;
+  by case: (comparableP z) => // [/lt_trans xlt/xlt|->] /ltW.
+Qed.
+
+Lemma comparable_le_minl : (min x y <= z) = (x <= z) || (y <= z).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; last rewrite orbC;
+  by move=> xy _; apply/idP/idP => [->|/orP[]]//; apply/le_trans/ltW.
+Qed.
+
+Lemma comparable_lt_minr : (z < min x y) = (z < x) && (z < y).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC;
+  by case: (comparableP z) => // /lt_trans xlt/xlt.
+Qed.
+
+Lemma comparable_lt_minl : (min x y < z) = (x < z) || (y < z).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; last rewrite orbC;
+  by move=> xy _; apply/idP/idP => [->|/orP[]]//; apply/lt_trans.
+Qed.
+
+Lemma comparable_le_maxr : (z <= max x y) = (z <= x) || (z <= y).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; first rewrite orbC;
+  by move=> xy _; apply/idP/idP => [->|/orP[]]// /le_trans->//; apply/ltW.
+Qed.
+
+Lemma comparable_le_maxl : (max x y <= z) = (x <= z) && (y <= z).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; first rewrite andbC;
+  by case: (comparableP z) => // [ylt /lt_trans /(_ _)/ltW|->/ltW]->.
+Qed.
+
+Lemma comparable_lt_maxr : (z < max x y) = (z < x) || (z < y).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; first rewrite orbC;
+  by move=> xy _; apply/idP/idP => [->|/orP[]]// /lt_trans->.
+Qed.
+
+Lemma comparable_lt_maxl : (max x y < z) = (x < z) && (y < z).
+Proof.
+case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; first rewrite andbC;
+by case: (comparableP z) => // ylt /lt_trans->.
+Qed.
+
+Lemma comparable_minxK : max (min x y) x = x.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
+
+Lemma comparable_minKx : max y (min x y) = y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
+
+Lemma comparable_maxxK : min (max x y) x = x.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
+
+Lemma comparable_maxKx : min y (max x y) = y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
+
+End Comparable2.
+
+Section Comparable3.
+Variables (x y z : T) (cmp_xy : x >=< y) (cmp_xz : x >=< z) (cmp_yz : y >=< z).
+Let P := comparableP.
+
+Lemma comparable_minA : min x (min y z) = min (min x y) z.
+Proof.
+move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=.
+move: (P x y) (P x z) (P y z) => [xy|xy|xy|<-] [xz|xz|xz|<-]// []//= yz.
+- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx.
+- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx.
+- by have := lt_trans xy xz; rewrite yz ltxx.
+Qed.
+
+Lemma comparable_maxA : max x (max y z) = max (max x y) z.
+Proof.
+move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=.
+move: (P x y) (P x z) (P y z) => [xy|xy|xy|<-] [xz|xz|xz|<-]// []//= yz.
+- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx.
+- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx.
+- by have := lt_trans xy xz; rewrite yz ltxx.
+Qed.
+
+Lemma comparable_max_minl : max (min x y) z = min (max x z) (max y z).
+Proof.
+move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=.
+move: (P x y) (P x z) (P y z).
+move=> [xy|xy|xy|<-] [xz|xz|xz|<-] [yz|yz|yz|//->]//= _; rewrite ?ltxx//.
+- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx.
+- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx.
+Qed.
+
+Lemma comparable_min_maxl : min (max x y) z = max (min x z) (min y z).
+Proof.
+move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=.
+move: (P x y) (P x z) (P y z).
+move=> [xy|xy|xy|<-] [xz|xz|xz|<-] []yz//= _; rewrite ?ltxx//.
+- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx.
+- by have := lt_trans xy yz; rewrite ltxx.
+- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx.
+- by have := lt_trans xy xz; rewrite yz ltxx.
+Qed.
+
+End Comparable3.
+
+Lemma comparable_minAC x y z : x >=< y -> x >=< z -> y >=< z ->
+  min (min x y) z = min (min x z) y.
+Proof.
+move=> xy xz yz; rewrite -comparable_minA// [min y z]comparable_minC//.
+by rewrite comparable_minA// 1?comparable_sym.
+Qed.
+
+Lemma comparable_maxAC x y z : x >=< y -> x >=< z -> y >=< z ->
+  max (max x y) z = max (max x z) y.
+Proof.
+move=> xy xz yz; rewrite -comparable_maxA// [max y z]comparable_maxC//.
+by rewrite comparable_maxA// 1?comparable_sym.
+Qed.
+
+Lemma comparable_minCA x y z : x >=< y -> x >=< z -> y >=< z ->
+  min x (min y z) = min y (min x z).
+Proof.
+move=> xy xz yz; rewrite comparable_minA// [min x y]comparable_minC//.
+by rewrite -comparable_minA// 1?comparable_sym.
+Qed.
+
+Lemma comparable_maxCA x y z : x >=< y -> x >=< z -> y >=< z ->
+  max x (max y z) = max y (max x z).
+Proof.
+move=> xy xz yz; rewrite comparable_maxA// [max x y]comparable_maxC//.
+by rewrite -comparable_maxA// 1?comparable_sym.
+Qed.
+
+Lemma comparable_minACA x y z t :
+    x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t ->
+  min (min x y) (min z t) = min (min x z) (min y t).
+Proof.
+move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//.
+rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//.
+by rewrite comparable_sym.
+Qed.
+
+Lemma comparable_maxACA x y z t :
+    x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t ->
+  max (max x y) (max z t) = max (max x z) (max y t).
+Proof.
+move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//.
+rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//.
+by rewrite comparable_sym.
+Qed.
+
+Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z ->
+  max x (min y z) = min (max x y) (max x z).
+Proof.
+move=> xy xz yz; rewrite ![max x _]comparable_maxC// ?comparable_minr//.
+by rewrite comparable_max_minl// 1?comparable_sym.
+Qed.
+
+Lemma comparable_min_maxr x y z : x >=< y -> x >=< z -> y >=< z ->
+  min x (max y z) = max (min x y) (min x z).
+Proof.
+move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//.
+by rewrite comparable_min_maxl// 1?comparable_sym.
+Qed.
+
+(* monotonicity *)
+
 Lemma mono_in_leif (A : {pred T}) (f : T -> T) C :
    {in A &, {mono f : x y / x <= y}} ->
   {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}.
@@ -3276,7 +3489,7 @@ Section TotalTheory.
 Context {disp : unit}.
 Local Notation orderType := (orderType disp).
 Context {T : orderType}.
-Implicit Types (x y z t : T).
+Implicit Types (x y z t : T) (s : seq T).
 
 Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed.
 Hint Resolve le_total : core.
@@ -3288,13 +3501,14 @@ Hint Resolve ge_total : core.
 Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed.
 Hint Resolve comparableT : core.
 
-Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s).
+Lemma sort_le_sorted s : sorted <=%O (sort <=%O s).
 Proof. exact: sort_sorted. Qed.
+Hint Resolve sort_le_sorted : core.
 
-Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s.
+Lemma sort_lt_sorted s : sorted lt (sort le s) = uniq s.
 Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed.
 
-Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s.
+Lemma sort_le_id s : sorted le s -> sort le s = s.
 Proof.
 by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort.
 Qed.
@@ -3340,19 +3554,91 @@ Proof. by move=> *; symmetry; apply: eq_ltLR. Qed.
 
 (* interaction with lattice operations *)
 
+Lemma meetEtotal x y : x `&` y = min x y. Proof. by case: leP. Qed.
+Lemma joinEtotal x y : x `|` y = max x y. Proof. by case: leP. Qed.
+
+Lemma minC : commutative (min : T -> T -> T).
+Proof. by move=> x y; apply: comparable_minC. Qed.
+
+Lemma maxC : commutative (max : T -> T -> T).
+Proof. by move=> x y; apply: comparable_maxC. Qed.
+
+Lemma minA : associative (min : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_minA. Qed.
+
+Lemma maxA : associative (max : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_maxA. Qed.
+
+Lemma minAC : right_commutative (min : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_minAC. Qed.
+
+Lemma maxAC : right_commutative (max : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_maxAC. Qed.
+
+Lemma minCA : left_commutative (min : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_minCA. Qed.
+
+Lemma maxCA : left_commutative (max : T -> T -> T).
+Proof. by move=> x y z; apply: comparable_maxCA. Qed.
+
+Lemma minACA : interchange (min : T -> T -> T) min.
+Proof. by move=> x y z t; apply: comparable_minACA. Qed.
+
+Lemma maxACA : interchange (max : T -> T -> T) max.
+Proof. by move=> x y z t; apply: comparable_maxACA. Qed.
+
+Lemma eq_minr x y : (min x y == y) = (y <= x).
+Proof. exact: comparable_eq_minr. Qed.
+
+Lemma eq_maxl x y : (max x y == x) = (y <= x).
+Proof. exact: comparable_eq_maxl. Qed.
+
+Lemma le_minr z x y : (z <= min x y) = (z <= x) && (z <= y).
+Proof. exact: comparable_le_minr. Qed.
+
+Lemma le_minl z x y : (min x y <= z) = (x <= z) || (y <= z).
+Proof. exact: comparable_le_minl. Qed.
+
+Lemma lt_minr z x y : (z < min x y) = (z < x) && (z < y).
+Proof. exact: comparable_lt_minr. Qed.
+
+Lemma lt_minl z x y : (min x y < z) = (x < z) || (y < z).
+Proof. exact: comparable_lt_minl. Qed.
+
+Lemma le_maxr z x y : (z <= max x y) = (z <= x) || (z <= y).
+Proof. exact: comparable_le_maxr. Qed.
+
+Lemma le_maxl z x y : (max x y <= z) = (x <= z) && (y <= z).
+Proof. exact: comparable_le_maxl. Qed.
+
+Lemma lt_maxr z x y : (z < max x y) = (z < x) || (z < y).
+Proof. exact: comparable_lt_maxr. Qed.
+
+Lemma lt_maxl z x y : (max x y < z) = (x < z) && (y < z).
+Proof. exact: comparable_lt_maxl. Qed.
+
+Lemma minxK x y : max (min x y) x = x. Proof. exact: comparable_minxK. Qed.
+Lemma minKx x y : max y (min x y) = y. Proof. exact: comparable_minKx. Qed.
+Lemma maxxK x y : min (max x y) x = x. Proof. exact: comparable_maxxK. Qed.
+Lemma maxKx x y : min y (max x y) = y. Proof. exact: comparable_maxKx. Qed.
+
+Lemma max_minl : left_distributive (max : T -> T -> T) min.
+Proof. by move=> x y z; apply: comparable_max_minl. Qed.
+
+Lemma min_maxl : left_distributive (min : T -> T -> T) max.
+Proof. by move=> x y z; apply: comparable_min_maxl. Qed.
+
+Lemma max_minr : right_distributive (max : T -> T -> T) min.
+Proof. by move=> x y z; apply: comparable_max_minr. Qed.
+
+Lemma min_maxr : right_distributive (min : T -> T -> T) max.
+Proof. by move=> x y z; apply: comparable_min_maxr. Qed.
+
 Lemma leIx x y z : (meet y z <= x) = (y <= x) || (z <= x).
-Proof.
-by case: (leP y z) => hyz; case: leP => ?;
-  rewrite ?(orbT, orbF) //=; apply/esym/negbTE;
-  rewrite -ltNge ?(lt_le_trans _ hyz) ?(lt_trans _ hyz).
-Qed.
+Proof. by rewrite meetEtotal le_minl. Qed.
 
 Lemma lexU x y z : (x <= join y z) = (x <= y) || (x <= z).
-Proof.
-by case: (leP y z) => hyz; case: leP => ?;
-  rewrite ?(orbT, orbF) //=; apply/esym/negbTE;
-  rewrite -ltNge ?(le_lt_trans hyz) ?(lt_trans hyz).
-Qed.
+Proof. by rewrite joinEtotal le_maxr. Qed.
 
 Lemma ltxI x y z : (x < meet y z) = (x < y) && (x < z).
 Proof. by rewrite !ltNge leIx negb_or. Qed.
@@ -3371,9 +3657,6 @@ Definition lteIx := (leIx, ltIx).
 Definition ltexU := (lexU, ltxU).
 Definition lteUx := (@leUx _ T, ltUx).
 
-Lemma meetEtotal x y : x `&` y = min x y. Proof. by case: leP. Qed.
-Lemma joinEtotal x y : x `|` y = max x y. Proof. by case: leP. Qed.
-
 Section ArgExtremum.
 
 Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).