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

5 files changed, 9 insertions, 11 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.