Improvements

- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update

7 files changed, 353 insertions, 317 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 41b5007..586b195 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -25,78 +25,71 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`,
     `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl`
 
-- in `order.v`, theory about for min and max
+- in `order.v`, defining `min` and `max` independently from `meet` and
+  `join`, and providing a theory about for min and max, hence generalizing
+  the theory of `Num.min` and `Num.max` from versions <= `1.10`, instead
+  of specializing to total order as in `1.11+beta1`:
   ```
-  Definition min x y := if x < y then x else y.
-  Definition max x y := if x < y then y else x.
-  ...
-  Definition meet := @min _ T.
-  Definition join := @max _ T.
+  Definition min (T : porderType) (x y : T) := if x < y then x else y.
+  Definition max (T : porderType) (x y : T) := if x < y then y else x.
   ```
-  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`,
-    `eq_minl`, `eq_maxr`, `comparable_minl`, `comparable_minr`,
-    `comparable_maxl`, `comparable_maxr`
-  + Lemmas under condition `x >=< y`:
+  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`, `eq_minl`, `eq_maxr`,
+    `min_idPl`, `max_idPr`, `min_minxK`, `min_minKx`, `max_maxxK`, `max_maxKx`,
+    `comparable_minl`, `comparable_minr`,  `comparable_maxl`, and `comparable_maxr`
+  + Lemmas about interaction with lattice operations:  `meetEtotal`, `joinEtotal`,
+  + Lemmas under condition of pairwise comparability of a (sub)set of their arguments:
     `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`,
-    `comparable_le_minr`, `comparable_le_minl`, `comparableP`, `comparable_lt_minr`,
+    `comparable_le_minr`, `comparable_le_minl`, `comparable_min_idPr`,
+    `comparable_max_idPl`, `comparableP`, `comparable_lt_minr`,
     `comparable_lt_minl`, `comparable_le_maxr`, `comparable_le_maxl`,
     `comparable_lt_maxr`, `comparable_lt_maxl`, `comparable_minxK`, `comparable_minKx`,
-    `comparable_maxxK`, `comparable_maxKx`
-  + Lemmas under conditions  x >=< y x >=< z y >=< z:
+    `comparable_maxxK`, `comparable_maxKx`,
     `comparable_minA`, `comparable_maxA`, `comparable_max_minl`, `comparable_min_maxl`,
     `comparable_minAC`, `comparable_maxAC`, `comparable_minCA`, `comparable_maxCA`,
     `comparable_minACA`, `comparable_maxACA`, `comparable_max_minr`, `comparable_min_maxr`
-  + Lemmas about interaction with lattice operations:
-    `meetEtotal`, `joinEtotal`, `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
-    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`, `le_minr`, `le_minl`,
-    `lt_minr`, `lt_minl`, `le_maxr`, `le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`,
+  + and the same but in a total order: `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
+    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`,
+    `min_idPr`, `max_idPl`, `le_minr`, `le_minl`, `lt_minr`,
+    `lt_minl`, `le_maxr`,`le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`,
     `maxxK`, `maxKx`, `max_minl`, `min_maxl`, `max_minr`, `min_maxr`
-- in `order.v`:
-  + in module `NatOrder`, added `nat_display` (instead of the now removed `total_display`)
-  + in module `BoolOrder`, added `bool_display` (instead of the now removed `total_display`)
-- in `ssrnum.v`, theory about min anx max:
+- in `ssrnum.v`, theory about `min` and `max` extended to `numDomainType`:
   + Lemmas: `real_oppr_max`, `real_oppr_min`, `real_addr_minl`, `real_addr_minr`,
     `real_addr_maxl`, `real_addr_maxr`, `minr_pmulr`, `maxr_pmulr`, `real_maxr_nmulr`,
     `real_minr_nmulr`, `minr_pmull`, `maxr_pmull`, `real_minr_nmull`, `real_maxr_nmull`,
     `real_maxrN`, `real_maxNr`, `real_minrN`, `real_minNr`
-- in `ssrnum.v`,
-  + new lemma: `comparable0r`
-  + in module `NumIntegralDomainTheory`:
-    ```
-    Definition minr x y := if x <= y then x else y.
-    Definition maxr x y := if x <= y then y else x.
-    ```
+- the compatibility module `ssrnum.mc_1_10` was extended to  support definitional
+  compatibility with `min` and `max` which had been lost in `1.11+beta1` for most instances.
 - in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE`
+- in `order.v`, new "unfolding" lemmas: `minEnat` and `maxEnat`
 
 ### Changed
 
 - in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`,
-  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters
-  + the following now deal with `min` and `max`
-    * `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP`
-    * `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP`
+  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters, so that the
+  the following now deal with `min` and `max`
+  + `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP`
+  + `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP`
 - in `order.v`:
-  + `[arg minr_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+  + `[arg min_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+  + `[arg max_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+  + added `comparable_arg_minP`,  `comparable_arg_maxP`,  `real_arg_minP`,  `real_arg_maxP`,
+    in order to take advantage of the former generalizations.
 - in `ssrnum.v`, `maxr` is a notation for `(@Order.max ring_display _)` (was `Order.join`)
   (resp. `minr` is a notation for `(@Order.min ring_display _)`)
 - in `ssrnum.v`, `ler_xor_gt`, `ltr_xor_ge`, `comparer`,
-  `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters
-  + the following now deal with min and max:
-    * `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P`
-    * `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P`
-- in `ssrnum.v`:
-  + `oppr_min` now restricted to the real subset
-  + the following have been redefined (were before derived from
-    `order.v` with `meet` and `join` lemmas):
-    * `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`,
-      `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC`
-    * `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`,
-      `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl`
-    * `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr`
-
-### Renamed
-
-- The added theories of min and max cause the following renamings:
+  `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters, so that
+  the following now deal with min and max:
+  + `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P`
+  + `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P`
+- in `ssrnum.v`, the following have been restated (which were formerly derived from
+  `order.v` and stated with specializations of the `meet` and `join` operators):
+   + `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`,
+     `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC`
+   + `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`,
+     `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl`
+   + `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr`
+- The new definitions of `min` and `max` may require the following rewrite rules
+  changes when dealing with `max` and `min` instead of `meet` and `join`:
   + `ltexI` -> `(le_minr,lt_minr)`
   + `lteIx` -> `(le_minl,lt_minl)`
   + `ltexU` -> `(le_maxr,lt_maxr)`
@@ -104,15 +97,25 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `lexU` -> `le_maxr`
   + `ltxU` -> `lt_maxr`
   + `lexU` -> `le_maxr`
+
+### Renamed
+
+- in `fintype` we deprecate and rename the following:
+  + `arg_minP` -> `arg_minnP`
+  + `arg_maxP` -> `arg_maxnP`
+
 - in `order.v`, in module `NatOrder`, renamings:
   + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`,
     `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`
 
 ### Removed
 
-- in `order.v`, removed `total_display` (was defining `max` using
-  `join` and `min` using `meet`)
+- in `order.v`, removed `total_display` (was used to provide the notation
+  `max` for `join` and `min` for `meet`).
 - in `order.v`, removed `minnE` and `maxnE`
+- in `order.v`,
+  + removed `meetEnat` (in favor of `meetEtotal` followed by `minEnat`)
+  + removed `joinEnat` (in favor of `joinEtotal` followed by `maxEnat`).
 
 ### Infrastructure
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index f7b2e0f..3bae08e 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -84,8 +84,7 @@ From mathcomp Require Import ssralg poly.
 (* and ><) and lattice operations (meet and join) defined in order.v are      *)
 (* redefined for the ring_display in the ring_scope (%R). 0-ary ordering      *)
 (* symbols for the ring_display have the suffix "%R", e.g., <%R. All the      *)
-(* other ordering notations are the same as order.v. The meet and join        *)
-(* operators for the ring_display are Num.min and Num.max.                    *)
+(* other ordering notations are the same as order.v.                          *)
 (*                                                                            *)
 (* Over these structures, we have the following operations                    *)
 (*             `|x| == norm of x.                                             *)
@@ -2877,6 +2876,24 @@ Proof.
 by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxrN ?realN.
 Qed.
 
+Section RealDomainArgExtremum.
+
+Context {I : finType} (i0 : I).
+Context (P : pred I) (F : I -> R) (Pi0 : P i0).
+Hypothesis F_real : {in P, forall i, F i \is real}.
+
+Lemma real_arg_minP : extremum_spec <=%R P F [arg min_(i < i0 | P i) F i].
+Proof.
+by apply: comparable_arg_minP => // i j iP jP; rewrite real_comparable ?F_real.
+Qed.
+
+Lemma real_arg_maxP : extremum_spec >=%R P F [arg max_(i > i0 | P i) F i].
+Proof.
+by apply: comparable_arg_maxP => // i j iP jP; rewrite real_comparable ?F_real.
+Qed.
+
+End RealDomainArgExtremum.
+
 (* norm *)
 
 Lemma real_ler_norm x : x \is real -> x <= `|x|.
@@ -3981,7 +3998,7 @@ Section MinMax.
 Lemma oppr_max : {morph -%R : x y / max x y >-> min x y : R}.
 Proof. by move=> x y; apply: real_oppr_max. Qed.
 
-Lemma oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}.
+Lemma oppr_min : {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.
@@ -5239,7 +5256,15 @@ Module Num.
 (* revert them in order to compile and commit.  This problem will be solved   *)
 (* in Coq 8.10.  See also: https://github.com/math-comp/math-comp/pull/270.   *)
 Export ssrnum.Num.
-Import ssrnum.Num.Def.
+
+Module Import Def.
+Export ssrnum.Num.Def.
+Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y.
+Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x.
+End Def.
+
+Notation min := minr.
+Notation max := maxr.
 
 Module Import Syntax.
 Notation "`| x |" :=
@@ -5294,11 +5319,7 @@ 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.
@@ -5611,14 +5632,11 @@ Variable R : realDomainType.
 Implicit Types x y z : R.
 Section MinMax.
 
-Let mrE x y : ((minr x y = min x y) * (maxr x y = max x y))%type.
+Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.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 minrC : @commutative R R min. Proof. mexact @minC. Qed.
 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.
@@ -5672,8 +5690,8 @@ Definition lter_minl := (ler_minl, ltr_minl).
 Definition lter_maxr := (ler_maxr, ltr_maxr).
 Definition lter_maxl := (ler_maxl, ltr_maxl).
 
-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 minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed.
+Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; 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.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index f0d432f..492aed8 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -506,7 +506,7 @@ have [r r_dv_p irr_r]: {r | r %| p & irreducible_poly r}.
   pose rVp (v : 'rV_n) (r := rVpoly v) := (1 < size r) && (r %| p).
   have [v0 Dp]: {v0 | rVpoly v0 = p & rVp v0}.
     by exists (poly_rV p); rewrite /rVp poly_rV_K ?C'p /=.
-  case/(arg_minP (size \o rVpoly))=> /= v; set r := rVpoly v.
+  case/(arg_minnP (size \o rVpoly))=> /= v; set r := rVpoly v.
   case/andP=> C'r r_dv_p min_r; exists r => //; split=> // q C'q q_dv_r.
   have nz_r: r != 0 by rewrite -size_poly_gt0 ltnW.
   have le_q_r: size q <= size r by rewrite dvdp_leq.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 95bc562..3a5caeb 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -264,7 +264,7 @@ Qed.
 
 Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}.
 Proof.
-move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order.
+move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 (mem G) order.
 exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT.
 apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p.
 rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr.
@@ -726,12 +726,12 @@ Qed.
 
 Lemma grank_min B : 'm(<<B>>) <= #|B|.
 Proof.
-by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid.
+by rewrite /gen_rank; case: arg_minnP => [|_ _ -> //]; rewrite genGid.
 Qed.
 
 Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}.
 Proof.
-rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid.
+rewrite /gen_rank; case: arg_minnP => [|B defG _]; first by rewrite genGid.
 by exists B; first apply/eqP.
 Qed.
 
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index e35d2c8..de03369 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1888,7 +1888,7 @@ Arguments bigmax_sup [I] i0 [P m F].
 Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F :
   P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
 Proof.
-move=> Pi0; case: arg_maxP => //= i Pi maxFi.
+move=> Pi0; case: arg_maxnP => //= i Pi maxFi.
 by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP.
 Qed.
 Arguments bigmax_eq_arg [I] i0 [P F].
@@ -1897,7 +1897,7 @@ Lemma eq_bigmax_cond (I : finType) (A : pred I) F :
   #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}.
 Proof.
 case: (pickP A) => [i0 Ai0 _ | ]; last by move/eq_card0->.
-by exists [arg max_(i > i0 in A) F i]; [case: arg_maxP | apply: bigmax_eq_arg].
+by exists [arg max_(i > i0 in A) F i]; [case: arg_maxnP | apply: bigmax_eq_arg].
 Qed.
 
 Lemma eq_bigmax (I : finType) F : #|I| > 0 -> {i0 : I | \max_i F i = F i0}.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index f69f336..abed211 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1636,10 +1636,10 @@ Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0).
 Definition arg_min := extremum leq i0 P F.
 Definition arg_max := extremum geq i0 P F.
 
-Lemma arg_minP : extremum_spec leq P F arg_min.
+Lemma arg_minnP : extremum_spec leq P F arg_min.
 Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed.
 
-Lemma arg_maxP : extremum_spec geq P F arg_max.
+Lemma arg_maxnP : extremum_spec geq P F arg_max.
 Proof.
 apply: extremumP => //; first exact: leqnn.
   by move=> n m p mn np; apply: leq_trans mn.
@@ -1650,6 +1650,13 @@ End ArgMinMax.
 
 End Extrema.
 
+Notation "@ 'arg_minP'" :=
+  (deprecate arg_minP arg_minnP) (at level 10, only parsing) : fun_scope.
+Notation arg_minP := (@arg_minP _ _ _) (only parsing).
+Notation "@ 'arg_maxP'" :=
+  (deprecate arg_maxP arg_maxnP) (at level 10, only parsing) : fun_scope.
+Notation arg_maxP := (@arg_maxP _ _ _) (only parsing).
+
 Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
     (arg_min i0 (fun i => P%B) (fun i => F))
   (at level 0, i, i0 at level 10,
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 59de10c..10a26f1 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -196,10 +196,10 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* above.                                                                     *)
 (*                                                                            *)
 (* For porderType we provide the following operations                         *)
-(*   [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to  *)
+(*   [arg min_(i < i0 | P) M] == a value i : T minimizing M : R, subject to   *)
 (*                      the condition P (i may appear in P and M), and        *)
 (*                      provided P holds for i0.                              *)
-(*   [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and     *)
+(*   [arg max_(i > i0 | P) M] == a value i maximizing M subject to P and      *)
 (*                      provided P holds for i0.                              *)
 (*   [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A.        *)
 (*   [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A.        *)
@@ -718,6 +718,43 @@ Reserved Notation "\min_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
            format "'[' \min_ ( i  'in'  A ) '/  '  F ']'").
 
+Reserved Notation "\max_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \max_ i '/  '  F ']'").
+Reserved Notation "\max_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \max_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\max_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \max_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\max_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \max_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\max_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \max_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\max_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \max_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\max_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\max_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\max_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \max_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\max_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \max_ ( i  <  n )  F ']'").
+Reserved Notation "\max_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \max_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\max_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \max_ ( i  'in'  A ) '/  '  F ']'").
+
 Reserved Notation "\meet^d_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \meet^d_ i '/  '  F ']'").
@@ -792,6 +829,80 @@ Reserved Notation "\join^d_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
            format "'[' \join^d_ ( i  'in'  A ) '/  '  F ']'").
 
+Reserved Notation "\min^d_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \min^d_ i '/  '  F ']'").
+Reserved Notation "\min^d_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \min^d_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \min^d_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \min^d_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \min^d_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \min^d_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\min^d_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\min^d_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \min^d_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \min^d_ ( i  <  n )  F ']'").
+Reserved Notation "\min^d_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \min^d_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\min^d_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \min^d_ ( i  'in'  A ) '/  '  F ']'").
+
+Reserved Notation "\max^d_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \max^d_ i '/  '  F ']'").
+Reserved Notation "\max^d_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \max^d_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \max^d_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \max^d_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \max^d_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \max^d_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\max^d_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\max^d_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \max^d_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \max^d_ ( i  <  n )  F ']'").
+Reserved Notation "\max^d_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \max^d_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\max^d_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \max^d_ ( i  'in'  A ) '/  '  F ']'").
+
 Reserved Notation "\meet^p_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \meet^p_ i '/  '  F ']'").
@@ -866,80 +977,6 @@ Reserved Notation "\join^p_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
            format "'[' \join^p_ ( i  'in'  A ) '/  '  F ']'").
 
-Reserved Notation "\min^l_ i F"
-  (at level 41, F at level 41, i at level 0,
-           format "'[' \min^l_ i '/  '  F ']'").
-Reserved Notation "\min^l_ ( i <- r | P ) F"
-  (at level 41, F at level 41, i, r at level 50,
-           format "'[' \min^l_ ( i  <-  r  |  P ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( i <- r ) F"
-  (at level 41, F at level 41, i, r at level 50,
-           format "'[' \min^l_ ( i  <-  r ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( m <= i < n | P ) F"
-  (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \min^l_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( m <= i < n ) F"
-  (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \min^l_ ( m  <=  i  <  n ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( i | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           format "'[' \min^l_ ( i  |  P ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
-Reserved Notation "\min^l_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
-Reserved Notation "\min^l_ ( i < n | P ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \min^l_ ( i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( i < n ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \min^l_ ( i  <  n )  F ']'").
-Reserved Notation "\min^l_ ( i 'in' A | P ) F"
-  (at level 41, F at level 41, i, A at level 50,
-           format "'[' \min^l_ ( i  'in'  A  |  P ) '/  '  F ']'").
-Reserved Notation "\min^l_ ( i 'in' A ) F"
-  (at level 41, F at level 41, i, A at level 50,
-           format "'[' \min^l_ ( i  'in'  A ) '/  '  F ']'").
-
-Reserved Notation "\max^l_ i F"
-  (at level 41, F at level 41, i at level 0,
-           format "'[' \max^l_ i '/  '  F ']'").
-Reserved Notation "\max^l_ ( i <- r | P ) F"
-  (at level 41, F at level 41, i, r at level 50,
-           format "'[' \max^l_ ( i  <-  r  |  P ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( i <- r ) F"
-  (at level 41, F at level 41, i, r at level 50,
-           format "'[' \max^l_ ( i  <-  r ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( m <= i < n | P ) F"
-  (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \max^l_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( m <= i < n ) F"
-  (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \max^l_ ( m  <=  i  <  n ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( i | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           format "'[' \max^l_ ( i  |  P ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
-Reserved Notation "\max^l_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
-Reserved Notation "\max^l_ ( i < n | P ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \max^l_ ( i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( i < n ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \max^l_ ( i  <  n )  F ']'").
-Reserved Notation "\max^l_ ( i 'in' A | P ) F"
-  (at level 41, F at level 41, i, A at level 50,
-           format "'[' \max^l_ ( i  'in'  A  |  P ) '/  '  F ']'").
-Reserved Notation "\max^l_ ( i 'in' A ) F"
-  (at level 41, F at level 41, i, A at level 50,
-           format "'[' \max^l_ ( i  'in'  A ) '/  '  F ']'").
-
 Module Order.
 
 (**************)
@@ -1066,11 +1103,13 @@ Variant incompare (x y : T) :
   | InCompareGt of y < x : incompare x y
     y y x x false false true false true false true true
   | InCompare of x >< y  : incompare x y
-    (min y x) (min x y) (max y x) (max x y)
-    false false false false false false false false
+    x y y x false false false false false false false false
   | InCompareEq of x = y : incompare x y
     x x x x true true true true false false true true.
 
+Definition arg_min {I : finType} := @extremum T I le.
+Definition arg_max {I : finType}  := @extremum T I ge.
+
 End POrderDef.
 
 Prenex Implicits lt le leif.
@@ -1130,6 +1169,34 @@ Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope.
 Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope.
 Notation "x >< y" := (~~ (comparable x y)) : order_scope.
 
+Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
+    (arg_min i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0  |  P )  F ]") : order_scope.
+
+Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
+    [arg min_(i < i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0  'in'  A )  F ]") : order_scope.
+
+Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0 )  F ]") : order_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
+     (arg_max i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0  |  P )  F ]") : order_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
+    [arg max_(i > i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0  'in'  A )  F ]") : order_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0 ) F ]") : order_scope.
+
 End POSyntax.
 
 Module POCoercions.
@@ -1244,8 +1311,7 @@ Variant incomparel (x y : T) :
   | InComparelGt of y < x : incomparel x y
     y y x x y y x x false false true false true false true true
   | InComparel of x >< y  : incomparel x y
-    (min y x) (min x y) (max y x) (max x y)
-    (meet y x) (meet x y) (join y x) (join x y)
+    x y y x (meet y x) (meet x y) (join y x) (join x y)
     false false false false false false false false
   | InComparelEq of x = y : incomparel x y
     x x x x x x x x true true true true false false true true.
@@ -1946,96 +2012,6 @@ End Exports.
 End Total.
 Import Total.Exports.
 
-Section TotalDef.
-Context {disp : unit} {T : orderType disp} {I : finType}.
-Definition arg_min := @extremum T I <=%O.
-Definition arg_max := @extremum T I >=%O.
-End TotalDef.
-
-Module Import TotalSyntax.
-
-Notation "\max_ ( i <- r | P ) F" :=
-  (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope.
-Notation "\max_ ( i <- r ) F" :=
-  (\big[max/0%O]_(i <- r) F%O) : order_scope.
-Notation "\max_ ( i | P ) F" :=
-  (\big[max/0%O]_(i | P%B) F%O) : order_scope.
-Notation "\max_ i F" :=
-  (\big[max/0%O]_i F%O) : order_scope.
-Notation "\max_ ( i : I | P ) F" :=
-  (\big[max/0%O]_(i : I | P%B) F%O) (only parsing) :
-  order_scope.
-Notation "\max_ ( i : I ) F" :=
-  (\big[max/0%O]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\max_ ( m <= i < n | P ) F" :=
-  (\big[max/0%O]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\max_ ( m <= i < n ) F" :=
-  (\big[max/0%O]_(m <= i < n) F%O) : order_scope.
-Notation "\max_ ( i < n | P ) F" :=
-  (\big[max/0%O]_(i < n | P%B) F%O) : order_scope.
-Notation "\max_ ( i < n ) F" :=
-  (\big[max/0%O]_(i < n) F%O) : order_scope.
-Notation "\max_ ( i 'in' A | P ) F" :=
-  (\big[max/0%O]_(i in A | P%B) F%O) : order_scope.
-Notation "\max_ ( i 'in' A ) F" :=
-  (\big[max/0%O]_(i in A) F%O) : order_scope.
-
-Notation "\min_ ( i <- r | P ) F" :=
-  (\big[min/1%O]_(i <- r | P%B) F%O) : order_scope.
-Notation "\min_ ( i <- r ) F" :=
-  (\big[min/1%O]_(i <- r) F%O) : order_scope.
-Notation "\min_ ( i | P ) F" :=
-  (\big[min/1%O]_(i | P%B) F%O) : order_scope.
-Notation "\min_ i F" :=
-  (\big[min/1%O]_i F%O) : order_scope.
-Notation "\min_ ( i : I | P ) F" :=
-  (\big[min/1%O]_(i : I | P%B) F%O) (only parsing) :
-  order_scope.
-Notation "\min_ ( i : I ) F" :=
-  (\big[min/1%O]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\min_ ( m <= i < n | P ) F" :=
-  (\big[min/1%O]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\min_ ( m <= i < n ) F" :=
-  (\big[min/1%O]_(m <= i < n) F%O) : order_scope.
-Notation "\min_ ( i < n | P ) F" :=
-  (\big[min/1%O]_(i < n | P%B) F%O) : order_scope.
-Notation "\min_ ( i < n ) F" :=
-  (\big[min/1%O]_(i < n) F%O) : order_scope.
-Notation "\min_ ( i 'in' A | P ) F" :=
-  (\big[min/1%O]_(i in A | P%B) F%O) : order_scope.
-Notation "\min_ ( i 'in' A ) F" :=
-  (\big[min/1%O]_(i in A) F%O) : order_scope.
-
-Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
-    (arg_min i0 (fun i => P%B) (fun i => F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'min_' ( i  <  i0  |  P )  F ]") : order_scope.
-
-Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
-    [arg min_(i < i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'min_' ( i  <  i0  'in'  A )  F ]") : order_scope.
-
-Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'min_' ( i  <  i0 )  F ]") : order_scope.
-
-Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
-     (arg_max i0 (fun i => P%B) (fun i => F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'max_' ( i  >  i0  |  P )  F ]") : order_scope.
-
-Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
-    [arg max_(i > i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'max_' ( i  >  i0  'in'  A )  F ]") : order_scope.
-
-Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg'  'max_' ( i  >  i0 ) F ]") : order_scope.
-
-End TotalSyntax.
-
 (**********)
 (* FINITE *)
 (**********)
@@ -2586,13 +2562,15 @@ Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope.
 Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope.
 Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope.
 
-Notation "x `&^d` y" :=  (@meet (dual_display _) _ x y) : order_scope.
-Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope.
-
 Notation dual_bottom := (@bottom (dual_display _)).
 Notation dual_top := (@top (dual_display _)).
 Notation dual_join := (@join (dual_display _) _).
 Notation dual_meet := (@meet (dual_display _) _).
+Notation dual_max := (@max (dual_display _) _).
+Notation dual_min := (@min (dual_display _) _).
+
+Notation "x `&^d` y" :=  (@meet (dual_display _) _ x y) : order_scope.
+Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope.
 
 Notation "\join^d_ ( i <- r | P ) F" :=
   (\big[join/0]_(i <- r | P%B) F%O) : order_scope.
@@ -2824,8 +2802,8 @@ Lemma comparableP x y : incompare x y
 Proof.
 rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y).
   by case: (comparable_ltgtP c_xy) => ?; constructor.
-by rewrite ?incomparable_eqF ?incomparable_leF ?incomparable_ltF //
-           1?comparable_sym //; constructor.
+by rewrite /min /max ?incomparable_eqF ?incomparable_leF;
+   rewrite ?incomparable_ltF// 1?comparable_sym //; constructor.
 Qed.
 
 Lemma le_comparable (x y : T) : x <= y -> x >=< y.
@@ -2882,6 +2860,24 @@ Proof. by move=> /eq_leif<-/eqP. Qed.
 
 (* min and max *)
 
+Lemma minElt x y : min x y = if x < y then x else y. Proof. by []. Qed.
+Lemma maxElt x y : max x y = if x < y then y else x. Proof. by []. Qed.
+
+Lemma minEle x y : min x y = if x <= y then x else y.
+Proof. by case: comparableP. Qed.
+
+Lemma maxEle x y : max x y = if x <= y then y else x.
+Proof. by case: comparableP. Qed.
+
+Lemma comparable_minEgt x y : x >=< y -> min x y = if x > y then y else x.
+Proof. by case: comparableP. Qed.
+Lemma comparable_maxEgt x y : x >=< y -> max x y = if x > y then x else y.
+Proof. by case: comparableP. Qed.
+Lemma comparable_minEge x y : x >=< y -> min x y = if x >= y then y else x.
+Proof. by case: comparableP. Qed.
+Lemma comparable_maxEge x y : x >=< y -> max x y = if x >= y then x else y.
+Proof. by case: comparableP. Qed.
+
 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.
@@ -2899,6 +2895,24 @@ 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 min_idPl x y : reflect (min x y = x) (x <= y).
+Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_minl. Qed.
+
+Lemma max_idPr x y : reflect (max x y = y) (x <= y).
+Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_maxr. Qed.
+
+Lemma min_minKx x y : min (min x y) y = min x y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed.
+
+Lemma min_minxK x y : min x (min x y) = min x y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed.
+
+Lemma max_maxKx x y : max (max x y) y = max x y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed.
+
+Lemma max_maxxK x y : max x (max x y) = max x y.
+Proof. by rewrite !(fun_if, if_arg) ltxx/=; 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.
 
@@ -2926,6 +2940,12 @@ 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_min_idPr : reflect (min x y = y) (y <= x).
+Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_minr. Qed.
+
+Lemma comparable_max_idPl : reflect (max x y = x) (y <= x).
+Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_maxl. Qed.
+
 Lemma comparable_le_minr : (z <= min x y) = (z <= x) && (z <= y).
 Proof.
 case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC;
@@ -2974,16 +2994,16 @@ 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.
+Lemma comparable_minxK : max (min x y) y = y.
 Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 
-Lemma comparable_minKx : max y (min x y) = y.
+Lemma comparable_minKx : max x (min x y) = x.
 Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 
-Lemma comparable_maxxK : min (max x y) x = x.
+Lemma comparable_maxxK : min (max x y) y = y.
 Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 
-Lemma comparable_maxKx : min y (max x y) = y.
+Lemma comparable_maxKx : min x (max x y) = x.
 Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 
 End Comparable2.
@@ -3092,6 +3112,24 @@ move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//.
 by rewrite comparable_min_maxl// 1?comparable_sym.
 Qed.
 
+Section ArgExtremum.
+
+Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).
+Hypothesis F_comparable : {in P &, forall i j, F i >=< F j}.
+
+Lemma comparable_arg_minP: extremum_spec <=%O P F (arg_min i0 P F).
+Proof.
+by apply: extremum_inP => // [x _|y x z _ _ _]; [apply: lexx|apply: le_trans].
+Qed.
+
+Lemma comparable_arg_maxP: extremum_spec >=%O P F (arg_max i0 P F).
+Proof.
+apply: extremum_inP => // [x _|y x z _ _ _|]; [exact: lexx|exact: ge_trans|].
+by move=> x y xP yP; rewrite orbC [_ || _]F_comparable.
+Qed.
+
+End ArgExtremum.
+
 (* monotonicity *)
 
 Lemma mono_in_leif (A : {pred T}) (f : T -> T) C :
@@ -3200,6 +3238,10 @@ Arguments mono_in_leif [disp T A f C].
 Arguments nmono_in_leif [disp T A f C].
 Arguments mono_leif [disp T f C].
 Arguments nmono_leif [disp T f C].
+Arguments min_idPl {disp T x y}.
+Arguments max_idPr {disp T x y}.
+Arguments comparable_min_idPr {disp T x y _}.
+Arguments comparable_max_idPl {disp T x y _}.
 
 Module Import DualPOrder.
 Section DualPOrder.
@@ -3458,6 +3500,9 @@ Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed.
 End LatticeTheoryJoin.
 End LatticeTheoryJoin.
 
+Arguments meet_idPl {disp L x y}.
+Arguments join_idPl {disp L x y}.
+
 Module Import DistrLatticeTheory.
 Section DistrLatticeTheory.
 Context {disp : unit}.
@@ -3554,11 +3599,18 @@ Lemma eq_ltRL x y z t :
   (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y).
 Proof. by move=> *; symmetry; apply: eq_ltLR. Qed.
 
-(* interaction with lattice operations *)
+(* max and min is join and meet *)
 
 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.
 
+(* max and min theory *)
+
+Lemma minEgt x y : min x y = if x > y then y else x. Proof. by case: ltP. Qed.
+Lemma maxEgt x y : max x y = if x > y then x else y. Proof. by case: ltP. Qed.
+Lemma minEge x y : min x y = if x >= y then y else x. Proof. by case: leP. Qed.
+Lemma maxEge x y : max x y = if x >= y then x else y. Proof. by case: leP. Qed.
+
 Lemma minC : commutative (min : T -> T -> T).
 Proof. by move=> x y; apply: comparable_minC. Qed.
 
@@ -3595,6 +3647,12 @@ Proof. exact: comparable_eq_minr. Qed.
 Lemma eq_maxl x y : (max x y == x) = (y <= x).
 Proof. exact: comparable_eq_maxl. Qed.
 
+Lemma min_idPr x y : reflect (min x y = y) (y <= x).
+Proof. exact: comparable_min_idPr. Qed.
+
+Lemma max_idPl x y : reflect (max x y = x) (y <= x).
+Proof. exact: comparable_max_idPl. Qed.
+
 Lemma le_minr z x y : (z <= min x y) = (z <= x) && (z <= y).
 Proof. exact: comparable_le_minr. Qed.
 
@@ -3619,10 +3677,10 @@ 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 minxK x y : max (min x y) y = y. Proof. exact: comparable_minxK. Qed.
+Lemma minKx x y : max x (min x y) = x. Proof. exact: comparable_minKx. Qed.
+Lemma maxxK x y : min (max x y) y = y. Proof. exact: comparable_maxxK. Qed.
+Lemma maxKx x y : min x (max x y) = x. 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.
@@ -3663,9 +3721,6 @@ Section ArgExtremum.
 
 Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).
 
-Definition arg_minnP := arg_minP.
-Definition arg_maxnP := arg_maxP.
-
 Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F).
 Proof. by apply: extremumP => //; apply: le_trans. Qed.
 
@@ -3675,6 +3730,10 @@ Proof. by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed.
 End ArgExtremum.
 
 End TotalTheory.
+
+Arguments min_idPr {disp T x y}.
+Arguments max_idPl {disp T x y}.
+
 Section TotalMonotonyTheory.
 
 Context {disp : unit} {disp' : unit}.
@@ -5402,61 +5461,11 @@ Notation "><^l x" := (fun y => ~~ (>=<^l%O x y)) : order_scope.
 Notation "><^l x :> T" := (><^l (x : T)) (only parsing) : order_scope.
 Notation "x ><^l y" := (~~ (><^l%O x y)) : order_scope.
 
-Notation minlexi := (@meet lexi_display _).
-Notation maxlexi := (@join lexi_display _).
-
-Notation "x `&^l` y" :=  (minlexi x y) : order_scope.
-Notation "x `|^l` y" := (maxlexi x y) : order_scope.
-
-Notation "\max^l_ ( i <- r | P ) F" :=
-  (\big[maxlexi/0]_(i <- r | P%B) F%O) : order_scope.
-Notation "\max^l_ ( i <- r ) F" :=
-  (\big[maxlexi/0]_(i <- r) F%O) : order_scope.
-Notation "\max^l_ ( i | P ) F" :=
-  (\big[maxlexi/0]_(i | P%B) F%O) : order_scope.
-Notation "\max^l_ i F" :=
-  (\big[maxlexi/0]_i F%O) : order_scope.
-Notation "\max^l_ ( i : I | P ) F" :=
-  (\big[maxlexi/0]_(i : I | P%B) F%O) (only parsing) : order_scope.
-Notation "\max^l_ ( i : I ) F" :=
-  (\big[maxlexi/0]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\max^l_ ( m <= i < n | P ) F" :=
- (\big[maxlexi/0]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\max^l_ ( m <= i < n ) F" :=
- (\big[maxlexi/0]_(m <= i < n) F%O) : order_scope.
-Notation "\max^l_ ( i < n | P ) F" :=
- (\big[maxlexi/0]_(i < n | P%B) F%O) : order_scope.
-Notation "\max^l_ ( i < n ) F" :=
- (\big[maxlexi/0]_(i < n) F%O) : order_scope.
-Notation "\max^l_ ( i 'in' A | P ) F" :=
- (\big[maxlexi/0]_(i in A | P%B) F%O) : order_scope.
-Notation "\max^l_ ( i 'in' A ) F" :=
- (\big[maxlexi/0]_(i in A) F%O) : order_scope.
-
-Notation "\min^l_ ( i <- r | P ) F" :=
-  (\big[minlexi/1]_(i <- r | P%B) F%O) : order_scope.
-Notation "\min^l_ ( i <- r ) F" :=
-  (\big[minlexi/1]_(i <- r) F%O) : order_scope.
-Notation "\min^l_ ( i | P ) F" :=
-  (\big[minlexi/1]_(i | P%B) F%O) : order_scope.
-Notation "\min^l_ i F" :=
-  (\big[minlexi/1]_i F%O) : order_scope.
-Notation "\min^l_ ( i : I | P ) F" :=
-  (\big[minlexi/1]_(i : I | P%B) F%O) (only parsing) : order_scope.
-Notation "\min^l_ ( i : I ) F" :=
-  (\big[minlexi/1]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\min^l_ ( m <= i < n | P ) F" :=
- (\big[minlexi/1]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\min^l_ ( m <= i < n ) F" :=
- (\big[minlexi/1]_(m <= i < n) F%O) : order_scope.
-Notation "\min^l_ ( i < n | P ) F" :=
- (\big[minlexi/1]_(i < n | P%B) F%O) : order_scope.
-Notation "\min^l_ ( i < n ) F" :=
- (\big[minlexi/1]_(i < n) F%O) : order_scope.
-Notation "\min^l_ ( i 'in' A | P ) F" :=
- (\big[minlexi/1]_(i in A | P%B) F%O) : order_scope.
-Notation "\min^l_ ( i 'in' A ) F" :=
- (\big[minlexi/1]_(i in A) F%O) : order_scope.
+Notation meetlexi := (@meet lexi_display _).
+Notation joinlexi := (@join lexi_display _).
+
+Notation "x `&^l` y" :=  (meetlexi x y) : order_scope.
+Notation "x `|^l` y" := (joinlexi x y) : order_scope.
 
 End LexiSyntax.
 
@@ -6997,7 +7006,6 @@ Export BLatticeSyntax.
 Export TBLatticeSyntax.
 Export CBDistrLatticeSyntax.
 Export CTBDistrLatticeSyntax.
-Export TotalSyntax.
 Export DualSyntax.
 Export DvdSyntax.
 End Syntax.