Add (meet|join)_(l|r), some renamings, and small cleanups

New lemmas:
- meet_l, meet_r, join_l, join_r.

Renamings:
- Order.BLatticeTheory.lexUl -> disjoint_lexUl,
- Order.BLatticeTheory.lexUr -> disjoint_lexUr,
- Order.TBLatticeTheory.lexIl -> cover_leIxl,
- Order.TBLatticeTheory.lexIr -> cover_leIxr.

Use `Order.TTheory` instead of `Order.Theory` if applicable

10 files changed, 36 insertions, 33 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index eaa256c..2a485fd 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -46,7 +46,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.Theory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Definition divz (m d : int) :=
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 48d5254..b34c1ad 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -40,7 +40,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Local Open Scope ring_scope.
-Import Order.Theory Order.Syntax GRing.Theory Num.Theory.
+Import Order.TTheory Order.Syntax GRing.Theory Num.Theory.
 
 Local Notation mid x y := ((x + y) / 2%:R).
 
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 4ef050f..8478d93 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -19,7 +19,7 @@ From mathcomp Require Import ssrint.
 (*       ratr x == generic embedding of  (r : R) into an arbitrary unitring.  *)
 (******************************************************************************)
 
-Import Order.Theory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index cbd6fa1..b408f9d 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -40,7 +40,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.Theory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory.
 Delimit Scope int_scope with Z.
 Local Open Scope int_scope.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index d068135..2906412 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -125,7 +125,7 @@ Unset Printing Implicit Defensive.
 
 Local Open Scope order_scope.
 Local Open Scope ring_scope.
-Import Order.Theory Order.Def Order.Syntax GRing.Theory.
+Import Order.TTheory Order.Def Order.Syntax GRing.Theory.
 
 Reserved Notation "<= y" (at level 35).
 Reserved Notation ">= y" (at level 35).
@@ -5478,12 +5478,12 @@ 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 := elimT meet_idPl.
-Definition minr_r x y : y <= x -> min x y = y := elimT meet_idPr.
+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 := elimT join_idPr.
-Definition maxr_r x y : x <= y -> max x y = y := elimT join_idPl.
+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.
@@ -5674,5 +5674,3 @@ Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F]
 
 End Num.
 End mc_1_9.
-
-Export mc_1_9 mc_1_9.Num.Syntax.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index e886c5a..faecc02 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -40,7 +40,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.Theory GroupScope GRing.Theory Num.Theory.
+Import Order.TTheory GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Section Basics.
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 8c1fd96..d41c6d8 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -53,7 +53,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.Theory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 (* The Num mixin for an algebraically closed field with an automorphism of    *)
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index e8521ec..613dd91 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -112,7 +112,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.Theory Order.Syntax GroupScope GRing.Theory Num.Theory.
+Import Order.TTheory Order.Syntax GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Local Notation "p ^ f" := (map_poly f p) : ring_scope.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index efe5cea..f0d432f 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -568,7 +568,7 @@ End FinFieldExists.
 
 Section FinDomain.
 
-Import order ssrnum ssrint algC cyclotomic Order.Theory Num.Theory.
+Import order ssrnum ssrint algC cyclotomic Order.TTheory Num.Theory.
 Local Infix "%|" := dvdn. (* Hide polynomial divisibility. *)
 
 Variable R : finUnitRingType.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index fd0f663..554ae72 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -783,14 +783,13 @@ Variable (disp : unit).
 Local Notation porderType := (porderType disp).
 Variable (T : porderType).
 
-Definition le (R : porderType) : rel R := POrder.le (POrder.class R).
+Definition le : rel T := POrder.le (POrder.class T).
 Local Notation "x <= y" := (le x y) : order_scope.
 
-Definition lt (R : porderType) : rel R := POrder.lt (POrder.class R).
+Definition lt : rel T := POrder.lt (POrder.class T).
 Local Notation "x < y" := (lt x y) : order_scope.
 
-Definition comparable (R : porderType) : rel R :=
-  fun (x y : R) => (x <= y) || (y <= x).
+Definition comparable : rel T := fun (x y : T) => (x <= y) || (y <= x).
 Local Notation "x >=< y" := (comparable x y) : order_scope.
 Local Notation "x >< y" := (~~ (x >=< y)) : order_scope.
 
@@ -1487,11 +1486,11 @@ Module Import TotalSyntax.
 Fact total_display : unit. Proof. exact: tt. Qed.
 
 Notation max := (@join total_display _).
-Notation "@ 'max' R" :=
-  (@join total_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'max' T" :=
+  (@join total_display T) (at level 10, T at level 8, only parsing).
 Notation min := (@meet total_display _).
-Notation "@ 'min' R" :=
-  (@meet total_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'min' T" :=
+  (@meet total_display T) (at level 10, T at level 8, only parsing).
 
 Notation "\max_ ( i <- r | P ) F" :=
   (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope.
@@ -1967,7 +1966,7 @@ Notation "x <=^c y <^c z" := ((x <=^c y) && (y <^c z)) : order_scope.
 Notation "x <^c y <^c z" := ((x <^c y) && (y <^c z)) : order_scope.
 
 Notation "x <=^c y ?= 'iff' C" := (<?=^c%O x y C) : order_scope.
-Notation "x <=^c y ?= 'iff' C :> R" := ((x : R) <=^c (y : R) ?= iff C)
+Notation "x <=^c y ?= 'iff' C :> T" := ((x : T) <=^c (y : T) ?= iff C)
   (only parsing) : order_scope.
 
 Notation ">=<^c x" := (>=<^c%O x) : order_scope.
@@ -2517,6 +2516,9 @@ Proof. by rewrite leEmeet; apply/eqP. Qed.
 Lemma meet_idPr {x y} : reflect (y `&` x = x) (x <= y).
 Proof. by rewrite meetC; apply/meet_idPl. Qed.
 
+Lemma meet_l x y : x <= y -> x `&` y = x. Proof. exact/meet_idPl. Qed.
+Lemma meet_r x y : y <= x -> x `&` y = y. Proof. exact/meet_idPr. Qed.
+
 Lemma leIidl x y : (x <= x `&` y) = (x <= y).
 Proof. by rewrite !leEmeet meetKI. Qed.
 Lemma leIidr x y : (x <= y `&` x) = (x <= y).
@@ -2582,6 +2584,9 @@ Proof. exact: (@meet_idPr _ [latticeType of L^c]). Qed.
 Lemma join_idPr {x y} : reflect (y `|` x = y) (x <= y).
 Proof. exact: (@meet_idPl _ [latticeType of L^c]). Qed.
 
+Lemma join_l x y : y <= x -> x `|` y = x. Proof. exact/join_idPr. Qed.
+Lemma join_r x y : x <= y -> x `|` y = y. Proof. exact/join_idPl. Qed.
+
 Lemma leUidl x y : (x `|` y <= y) = (x <= y).
 Proof. exact: (@leIidr _ [latticeType of L^c]). Qed.
 Lemma leUidr x y : (y `|` x <= y) = (x <= y).
@@ -2809,14 +2814,14 @@ Qed.
 Lemma leU2r_le y t x z : x `&` t = 0 -> y `|` x <= t `|` z -> x <= z.
 Proof. by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed.
 
-Lemma lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y).
+Lemma disjoint_lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y).
 Proof.
 move=> xz0; apply/idP/idP=> xy; last by rewrite lexU2 ?xy.
 by apply: (@leU2l_le x z); rewrite ?joinxx.
 Qed.
 
-Lemma lexUr z x y : x `&` z = 0 -> (x <= z `|` y) = (x <= y).
-Proof. by move=> xz0; rewrite joinC; rewrite lexUl. Qed.
+Lemma disjoint_lexUr z x y : x `&` z = 0 -> (x <= z `|` y) = (x <= y).
+Proof. by move=> xz0; rewrite joinC; rewrite disjoint_lexUl. Qed.
 
 Lemma leU2E x y z t : x `&` t = 0 -> y `&` z = 0 ->
   (x `|` y <= z `|` t) = (x <= z) && (y <= t).
@@ -2970,11 +2975,11 @@ Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^c]). Qed.
 Lemma leI2r_le y t x z : y `|` z = 1 -> y `&` x <= t `&` z -> x <= z.
 Proof. rewrite joinC; exact: (@leU2r_le _ [tblatticeType of L^c]). Qed.
 
-Lemma lexIl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y).
-Proof. rewrite joinC; exact: (@lexUl _ [tblatticeType of L^c]). Qed.
+Lemma cover_leIxl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y).
+Proof. rewrite joinC; exact: (@disjoint_lexUl _ [tblatticeType of L^c]). Qed.
 
-Lemma lexIr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y).
-Proof. rewrite joinC; exact: (@lexUr _ [tblatticeType of L^c]). Qed.
+Lemma cover_leIxr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y).
+Proof. rewrite joinC; exact: (@disjoint_lexUr _ [tblatticeType of L^c]). Qed.
 
 Lemma leI2E x y z t : x `|` t = 1 -> y `|` z = 1 ->
   (x `&` y <= z `&` t) = (x <= z) && (y <= t).
@@ -3943,7 +3948,7 @@ Notation "x <=^p y <^p z" := ((x <=^p y) && (y <^p z)) : order_scope.
 Notation "x <^p y <^p z" := ((x <^p y) && (y <^p z)) : order_scope.
 
 Notation "x <=^p y ?= 'iff' C" := (<?=^p%O x y C) : order_scope.
-Notation "x <=^p y ?= 'iff' C :> R" := ((x : R) <=^p (y : R) ?= iff C)
+Notation "x <=^p y ?= 'iff' C :> T" := ((x : T) <=^p (y : T) ?= iff C)
   (only parsing) : order_scope.
 
 Notation ">=<^p x" := (>=<^p%O x) : order_scope.
@@ -4052,7 +4057,7 @@ Notation "x <=^l y <^l z" := ((x <=^l y) && (y <^l z)) : order_scope.
 Notation "x <^l y <^l z" := ((x <^l y) && (y <^l z)) : order_scope.
 
 Notation "x <=^l y ?= 'iff' C" := (<?=^l%O x y C) : order_scope.
-Notation "x <=^l y ?= 'iff' C :> R" := ((x : R) <=^l (y : R) ?= iff C)
+Notation "x <=^l y ?= 'iff' C :> T" := ((x : T) <=^l (y : T) ?= iff C)
   (only parsing) : order_scope.
 
 Notation ">=<^l x" := (>=<^l%O x) : order_scope.