Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341)

ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
  which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
  (to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
  from fewer axioms.

order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
  top and bottom elements except for empty set. Therefore we removed finite
  lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
  + `LTheory` (lattice and partial order, without complement and totality)
  + `CTheory` (`LTheory` + complement)
  + `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
  Products and lists can be ordered in two different ways: the lexicographical
  ordering and the pointwise ordering. Now their canonical instances are not
  exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.

General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
  like lemmas:
  lt_def    x y : (x < y) = (y != x) && (x <= y),
  lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
  + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
    aliases of `meet` and `join` specialized for `total_display`.
  + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
    `comparable` notations and their explicit variants in `Num.Def`.
  + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
    notations in `nat_scope` (specialized for nat), `order_scope` (general
    version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.

3 files changed, 1985 insertions, 1105 deletions

diff --git a/mathcomp/ssreflect/all_ssreflect.v b/mathcomp/ssreflect/all_ssreflect.v
index aae57ca..318d5ef 100644
--- a/mathcomp/ssreflect/all_ssreflect.v
+++ b/mathcomp/ssreflect/all_ssreflect.v
@@ -14,5 +14,6 @@ Require Export finfun.
 Require Export bigop.
 Require Export prime.
 Require Export finset.
+Require Export order.
 Require Export binomial.
 Require Export generic_quotient.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index b6f618d..5a42c80 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1051,16 +1051,16 @@ End Extremum.
 Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
     (extremum ord i0 (fun i => P%B) (fun i => F))
   (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i  <  i0  |  P )  F ]") : form_scope.
+   format "[ 'arg[' ord ]_( i  <  i0  |  P )  F ]") : nat_scope.
 
 Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" :=
     [arg[ord]_(i < i0 | i \in A) F]
   (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i  <  i0  'in'  A )  F ]") : form_scope.
+   format "[ 'arg[' ord ]_( i  <  i0  'in'  A )  F ]") : nat_scope.
 
 Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F]
   (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i  <  i0 )  F ]") : form_scope.
+   format "[ 'arg[' ord ]_( i  <  i0 )  F ]") : nat_scope.
 
 Section ArgMinMax.
 
@@ -1086,30 +1086,30 @@ End Extrema.
 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 ]") : form_scope.
+   format "[ 'arg'  'min_' ( i  <  i0  |  P )  F ]") : nat_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 ]") : form_scope.
+   format "[ 'arg'  'min_' ( i  <  i0  'in'  A )  F ]") : nat_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 ]") : form_scope.
+   format "[ 'arg'  'min_' ( i  <  i0 )  F ]") : nat_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 ]") : form_scope.
+   format "[ 'arg'  'max_' ( i  >  i0  |  P )  F ]") : nat_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 ]") : form_scope.
+   format "[ 'arg'  'max_' ( i  >  i0  'in'  A )  F ]") : nat_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 ]") : form_scope.
+   format "[ 'arg'  'max_' ( i  >  i0 ) F ]") : nat_scope.
 
 (**********************************************************************)
 (*                                                                    *)
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index cd8d8d8..d6202c3 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -17,61 +17,103 @@
 (* You should have received a copy of the GNU General Public License     *)
 (* along with this program.  If not, see <http://www.gnu.org/licenses/>. *)
 (*************************************************************************)
-
-From mathcomp
-Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq.
-From mathcomp
-Require Import fintype tuple bigop path finset.
-
-(*****************************************************************************)
-(* This files definies a ordered and decidable relations on a                *)
-(* type as canonical structure.  One need to import Order.Theory to get      *)
-(* the theory of such relations. The scope order_scope (%O) contains         *)
-(* fancier notation for this kind of ordeering.                              *)
-(*                                                                           *)
-(*          porderType == the type of partially ordered types                *)
-(*           orderType == the type of totally ordered types                  *)
-(*         latticeType == the type of distributive lattices                  *)
-(*        blatticeType == ... with a bottom elemnt                           *)
-(*        tlatticeType == ... with a top element                             *)
-(*       tblatticeType == ... with both a top and a bottom                   *)
-(*       cblatticeType == ... with a complement to, and bottom               *)
-(*      tcblatticeType == ... with a top, bottom, and general complement     *)
-(*                                                                           *)
-(* Each of these structure take a first argument named display, of type unit *)
-(* instanciating it with tt or an unknown key will lead to a default display *)
-(* Optionally, one can configure the display by setting one owns notation    *)
-(* on operators instanciated for their particular display                    *)
-(* One example of this is the reverse display ^r, every notation with the    *)
-(* suffix ^r (e.g. x <=^r y) is about the reversal order, in order not to    *)
-(* confuse the normal order with its reversal.                               *)
-(*                                                                           *)
-(* PorderType pord_mixin == builds an ordtype from a a partial order mixin   *)
-(*                          containing le, lt and refl, antisym, trans of le *)
-(* LatticeType lat_mixin == builds a distributive lattice from a porderType  *)
-(*                          meet and join and axioms                         *)
-(*    OrderType le_total == builds an order type from a lattice              *)
-(*                          and from a proof of totality                     *)
-(*                  ...                                                      *)
-(*                                                                           *)
-(* We provide a canonical structure of orderType for natural numbers (nat)   *)
-(* for finType and for pairs of ordType by lexicographic orderering.         *)
-(*                                                                           *)
-(* leP ltP ltgtP are the three main lemmas for case analysis                 *)
-(*                                                                           *)
-(* We also provide specialized version of some theorems from path.v.         *)
-(*                                                                           *)
-(* There are three distinct uses of the symbols <, <=, > and >=:             *)
-(*    0-ary, unary (prefix) and binary (infix).                              *)
-(* 0. <%O, <=%O, >%O, >=%O stand respectively for lt, le, gt and ge.         *)
-(* 1. (< x),  (<= x), (> x),  (>= x) stand respectively for                  *)
-(*    (gt x), (ge x), (lt x), (le x).                                        *)
-(*    So (< x) is a predicate characterizing elements smaller than x.        *)
-(* 2. (x < y), (x <= y), ... mean what they are expected to.                 *)
-(*  These convention are compatible with haskell's,                          *)
-(*   where ((< y) x) = (x < y) = ((<) x y),                                  *)
-(*   except that we write <%O instead of (<).                                *)
-(*****************************************************************************)
+From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq.
+From mathcomp Require Import fintype tuple bigop path finset.
+
+(******************************************************************************)
+(* This files definies a ordered and decidable relations on a type as         *)
+(* canonical structure.  One need to import some of the following modules to  *)
+(* get the definitions, notations, and theory of such relations.              *)
+(*       Order.Def: definitions of basic operations.                          *)
+(*    Order.Syntax: fancy notations for ordering declared in the order_scope  *)
+(*                  (%O).                                                     *)
+(*   Order.LTheory: theory of partially ordered types and lattices excluding  *)
+(*                  complement and totality related theorems.                 *)
+(*   Order.CTheory: theory of complemented lattices including Order.LTheory.  *)
+(*   Order.TTheory: theory of totally ordered types including Order.LTheory.  *)
+(*    Order.Theory: theory of ordered types including all of the above        *)
+(*                  theory modules.                                           *)
+(*                                                                            *)
+(* We provide the following structures of ordered types                       *)
+(*        porderType == the type of partially ordered types                   *)
+(*         orderType == the type of totally ordered types                     *)
+(*       latticeType == the type of distributive lattices                     *)
+(*      blatticeType == ... with a bottom elemnt                              *)
+(*     tblatticeType == ... with both a top and a bottom                      *)
+(*     cblatticeType == the type of sectionally complemented lattices         *)
+(*                      (lattices with a complement to, and bottom)           *)
+(*    ctblatticeType == the type of complemented lattices                     *)
+(*                      (lattices with a top, bottom, and general complement) *)
+(*    finPOerderType == the type of partially ordered finite types            *)
+(*    finLatticeType == the type of nonempty finite lattices                  *)
+(*   finClatticeType == the type of nonempty finite complemented lattices     *)
+(*      finOrderType == the type of nonempty totally ordered finite types     *)
+(*                                                                            *)
+(* Each of these structure take a first argument named display, of type unit  *)
+(* instanciating it with tt or an unknown key will lead to a default display. *)
+(* Optionally, one can configure the display by setting one owns notation on  *)
+(* operators instanciated for their particular display.                       *)
+(* One example of this is the converse display ^c, every notation with the    *)
+(* suffix ^c (e.g. x <=^c y) is about the converse order, in order not to     *)
+(* confuse the normal order with its converse.                                *)
+(*                                                                            *)
+(* PorderType pord_mixin == builds a porderType from a partial order mixin    *)
+(*                          containing le, lt and refl, antisym, trans of le  *)
+(* LatticeType lat_mixin == builds a distributive lattice from a porderType   *)
+(*                          meet and join and axioms                          *)
+(*    OrderType le_total == builds an order type from a latticeType and from  *)
+(*                          a proof of totality                               *)
+(*                  ...                                                       *)
+(*                                                                            *)
+(* Over these structures, we have the following operations                    *)
+(*            x <= y <-> x is less than or equal to y.                        *)
+(*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
+(*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
+(*             x > y <-> x is greater than y (:= y < x).                      *)
+(*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
+(*           x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)).    *)
+(*            x >< y <-> x and y are incomparable.                            *)
+(* For lattices we provide the following operations                           *)
+(*           x `&` y == the meet of x and y.                                  *)
+(*           x `|` y == the join of x and y.                                  *)
+(*                 0 == the bottom element.                                   *)
+(*                 1 == the top element.                                      *)
+(*           x `\` y == the (sectional) complement of y in [0, x].            *)
+(*              ~` x == the complement of x in [0, 1].                        *)
+(*   \meet_<range> e == iterated meet of a lattice with a top.                *)
+(*   \join_<range> e == iterated join of a lattice with a bottom.             *)
+(* For orderType we provide the following operations                          *)
+(*   [arg minr_(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     *)
+(*                      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.        *)
+(*   [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T.             *)
+(*   [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T.             *)
+(*                                                                            *)
+(* There are three distinct uses of the symbols                               *)
+(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><:                                *)
+(*    0-ary, unary (prefix), and binary (infix).                              *)
+(* 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for     *)
+(*    lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable.   *)
+(* 1. (< x),  (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively   *)
+(*    for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x).      *)
+(*    So (< x) is a predicate characterizing elements smaller than x.         *)
+(* 2. (x < y), (x <= y), ... mean what they are expected to.                  *)
+(*  These convention are compatible with Haskell's,                           *)
+(*   where ((< y) x) = (x < y) = ((<) x y),                                   *)
+(*   except that we write <%O instead of (<).                                 *)
+(*                                                                            *)
+(* We provide the following canonical instances of ordered types              *)
+(* - porderType, latticeType, orderType, blatticeType of nat                  *)
+(* - porderType of seq (lexicographic ordering)                               *)
+(*                                                                            *)
+(* leP ltP ltgtP are the three main lemmas for case analysis.                 *)
+(*                                                                            *)
+(* We also provide specialized version of some theorems from path.v.          *)
+(******************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -95,37 +137,37 @@ Reserved Notation "x >< y" (at level 70, no associativity).
 Reserved Notation ">< x" (at level 35).
 Reserved Notation ">< y :> T" (at level 35, y at next level).
 
-Reserved Notation "x <=^r y" (at level 70, y at next level).
-Reserved Notation "x >=^r y" (at level 70, y at next level, only parsing).
-Reserved Notation "x <^r y" (at level 70, y at next level).
-Reserved Notation "x >^r y" (at level 70, y at next level, only parsing).
-Reserved Notation "x <=^r y :> T" (at level 70, y at next level).
-Reserved Notation "x >=^r y :> T" (at level 70, y at next level, only parsing).
-Reserved Notation "x <^r y :> T" (at level 70, y at next level).
-Reserved Notation "x >^r y :> T" (at level 70, y at next level, only parsing).
-Reserved Notation "<=^r y" (at level 35).
-Reserved Notation ">=^r y" (at level 35).
-Reserved Notation "<^r y" (at level 35).
-Reserved Notation ">^r y" (at level 35).
-Reserved Notation "<=^r y :> T" (at level 35, y at next level).
-Reserved Notation ">=^r y :> T" (at level 35, y at next level).
-Reserved Notation "<^r y :> T" (at level 35, y at next level).
-Reserved Notation ">^r y :> T" (at level 35, y at next level).
-Reserved Notation "x >=<^r y" (at level 70, no associativity).
-Reserved Notation ">=<^r x" (at level 35).
-Reserved Notation ">=<^r y :> T" (at level 35, y at next level).
-Reserved Notation "x ><^r y" (at level 70, no associativity).
-Reserved Notation "><^r x" (at level 35).
-Reserved Notation "><^r y :> T" (at level 35, y at next level).
-
-Reserved Notation "x <=^r y <=^r z" (at level 70, y, z at next level).
-Reserved Notation "x <^r y <=^r z" (at level 70, y, z at next level).
-Reserved Notation "x <=^r y <^r z" (at level 70, y, z at next level).
-Reserved Notation "x <^r y <^r z" (at level 70, y, z at next level).
-Reserved Notation "x <=^r y ?= 'iff' c" (at level 70, y, c at next level,
-  format "x '[hv'  <=^r  y '/'  ?=  'iff'  c ']'").
-Reserved Notation "x <=^r y ?= 'iff' c :> T" (at level 70, y, c at next level,
-  format "x '[hv'  <=^r  y '/'  ?=  'iff'  c  :> T ']'").
+Reserved Notation "x <=^c y" (at level 70, y at next level).
+Reserved Notation "x >=^c y" (at level 70, y at next level, only parsing).
+Reserved Notation "x <^c y" (at level 70, y at next level).
+Reserved Notation "x >^c y" (at level 70, y at next level, only parsing).
+Reserved Notation "x <=^c y :> T" (at level 70, y at next level).
+Reserved Notation "x >=^c y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x <^c y :> T" (at level 70, y at next level).
+Reserved Notation "x >^c y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "<=^c y" (at level 35).
+Reserved Notation ">=^c y" (at level 35).
+Reserved Notation "<^c y" (at level 35).
+Reserved Notation ">^c y" (at level 35).
+Reserved Notation "<=^c y :> T" (at level 35, y at next level).
+Reserved Notation ">=^c y :> T" (at level 35, y at next level).
+Reserved Notation "<^c y :> T" (at level 35, y at next level).
+Reserved Notation ">^c y :> T" (at level 35, y at next level).
+Reserved Notation "x >=<^c y" (at level 70, no associativity).
+Reserved Notation ">=<^c x" (at level 35).
+Reserved Notation ">=<^c y :> T" (at level 35, y at next level).
+Reserved Notation "x ><^c y" (at level 70, no associativity).
+Reserved Notation "><^c x" (at level 35).
+Reserved Notation "><^c y :> T" (at level 35, y at next level).
+
+Reserved Notation "x <=^c y <=^c z" (at level 70, y, z at next level).
+Reserved Notation "x <^c y <=^c z" (at level 70, y, z at next level).
+Reserved Notation "x <=^c y <^c z" (at level 70, y, z at next level).
+Reserved Notation "x <^c y <^c z" (at level 70, y, z at next level).
+Reserved Notation "x <=^c y ?= 'iff' c" (at level 70, y, c at next level,
+  format "x '[hv'  <=^c  y '/'  ?=  'iff'  c ']'").
+Reserved Notation "x <=^c y ?= 'iff' c :> T" (at level 70, y, c at next level,
+  format "x '[hv'  <=^c  y '/'  ?=  'iff'  c  :> T ']'").
 
 (* Reserved notation for lattice operations. *)
 Reserved Notation "A `&` B"  (at level 48, left associativity).
@@ -133,11 +175,11 @@ Reserved Notation "A `|` B" (at level 52, left associativity).
 Reserved Notation "A `\` B" (at level 50, left associativity).
 Reserved Notation "~` A" (at level 35, right associativity).
 
-(* Reserved notation for reverse lattice operations. *)
-Reserved Notation "A `&^r` B"  (at level 48, left associativity).
-Reserved Notation "A `|^r` B" (at level 52, left associativity).
-Reserved Notation "A `\^r` B" (at level 50, left associativity).
-Reserved Notation "~^r` A" (at level 35, right associativity).
+(* Reserved notation for converse lattice operations. *)
+Reserved Notation "A `&^c` B"  (at level 48, left associativity).
+Reserved Notation "A `|^c` B" (at level 52, left associativity).
+Reserved Notation "A `\^c` B" (at level 50, left associativity).
+Reserved Notation "~^c` A" (at level 35, right associativity).
 
 Reserved Notation "\meet_ i F"
   (at level 41, F at level 41, i at level 0,
@@ -213,82 +255,79 @@ Reserved Notation "\join_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
            format "'[' \join_ ( i  'in'  A ) '/  '  F ']'").
 
-Reserved Notation "\meet^r_ i F"
+Reserved Notation "\meet^c_ i F"
   (at level 41, F at level 41, i at level 0,
-           format "'[' \meet^r_ i '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i <- r | P ) F"
+           format "'[' \meet^c_ i '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i <- r | P ) F"
   (at level 41, F at level 41, i, r at level 50,
-           format "'[' \meet^r_ ( i  <-  r  |  P ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i <- r ) F"
+           format "'[' \meet^c_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i <- r ) F"
   (at level 41, F at level 41, i, r at level 50,
-           format "'[' \meet^r_ ( i  <-  r ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( m <= i < n | P ) F"
+           format "'[' \meet^c_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( m <= i < n | P ) F"
   (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \meet^r_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( m <= i < n ) F"
+           format "'[' \meet^c_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( m <= i < n ) F"
   (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \meet^r_ ( m  <=  i  <  n ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i | P ) F"
+           format "'[' \meet^c_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
-           format "'[' \meet^r_ ( i  |  P ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i : t | P ) F"
+           format "'[' \meet^c_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i : t | P ) F"
   (at level 41, F at level 41, i at level 50,
            only parsing).
-Reserved Notation "\meet^r_ ( i : t ) F"
+Reserved Notation "\meet^c_ ( i : t ) F"
   (at level 41, F at level 41, i at level 50,
            only parsing).
-Reserved Notation "\meet^r_ ( i < n | P ) F"
+Reserved Notation "\meet^c_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
-           format "'[' \meet^r_ ( i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i < n ) F"
+           format "'[' \meet^c_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
-           format "'[' \meet^r_ ( i  <  n )  F ']'").
-Reserved Notation "\meet^r_ ( i 'in' A | P ) F"
+           format "'[' \meet^c_ ( i  <  n )  F ']'").
+Reserved Notation "\meet^c_ ( i 'in' A | P ) F"
   (at level 41, F at level 41, i, A at level 50,
-           format "'[' \meet^r_ ( i  'in'  A  |  P ) '/  '  F ']'").
-Reserved Notation "\meet^r_ ( i 'in' A ) F"
+           format "'[' \meet^c_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\meet^c_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
-           format "'[' \meet^r_ ( i  'in'  A ) '/  '  F ']'").
+           format "'[' \meet^c_ ( i  'in'  A ) '/  '  F ']'").
 
-Reserved Notation "\join^r_ i F"
+Reserved Notation "\join^c_ i F"
   (at level 41, F at level 41, i at level 0,
-           format "'[' \join^r_ i '/  '  F ']'").
-Reserved Notation "\join^r_ ( i <- r | P ) F"
+           format "'[' \join^c_ i '/  '  F ']'").
+Reserved Notation "\join^c_ ( i <- r | P ) F"
   (at level 41, F at level 41, i, r at level 50,
-           format "'[' \join^r_ ( i  <-  r  |  P ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( i <- r ) F"
+           format "'[' \join^c_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( i <- r ) F"
   (at level 41, F at level 41, i, r at level 50,
-           format "'[' \join^r_ ( i  <-  r ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( m <= i < n | P ) F"
+           format "'[' \join^c_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( m <= i < n | P ) F"
   (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \join^r_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( m <= i < n ) F"
+           format "'[' \join^c_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( m <= i < n ) F"
   (at level 41, F at level 41, i, m, n at level 50,
-           format "'[' \join^r_ ( m  <=  i  <  n ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( i | P ) F"
+           format "'[' \join^c_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
-           format "'[' \join^r_ ( i  |  P ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( i : t | P ) F"
+           format "'[' \join^c_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( i : t | P ) F"
   (at level 41, F at level 41, i at level 50,
            only parsing).
-Reserved Notation "\join^r_ ( i : t ) F"
+Reserved Notation "\join^c_ ( i : t ) F"
   (at level 41, F at level 41, i at level 50,
            only parsing).
-Reserved Notation "\join^r_ ( i < n | P ) F"
+Reserved Notation "\join^c_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
-           format "'[' \join^r_ ( i  <  n  |  P ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( i < n ) F"
+           format "'[' \join^c_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
-           format "'[' \join^r_ ( i  <  n )  F ']'").
-Reserved Notation "\join^r_ ( i 'in' A | P ) F"
+           format "'[' \join^c_ ( i  <  n )  F ']'").
+Reserved Notation "\join^c_ ( i 'in' A | P ) F"
   (at level 41, F at level 41, i, A at level 50,
-           format "'[' \join^r_ ( i  'in'  A  |  P ) '/  '  F ']'").
-Reserved Notation "\join^r_ ( i 'in' A ) F"
+           format "'[' \join^c_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\join^c_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
-           format "'[' \join^r_ ( i  'in'  A ) '/  '  F ']'").
-
-Fact unit_irrelevance (x y : unit) : x = y.
-Proof. by case: x; case: y. Qed.
+           format "'[' \join^c_ ( i  'in'  A ) '/  '  F ']'").
 
 Module Order.
 
@@ -298,10 +337,10 @@ Module Order.
 
 Module POrder.
 Section ClassDef.
-Structure mixin_of (T : eqType) := Mixin {
+Record mixin_of (T : eqType) := Mixin {
   le : rel T;
   lt : rel T;
-  _  : forall x y, lt x y = (x != y) && (le x y);
+  _  : forall x y, lt x y = (y != x) && (le x y);
   _  : reflexive     le;
   _  : antisymmetric le;
   _  : transitive    le
@@ -321,54 +360,53 @@ Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (disp : unit) (cT : type disp).
 
 Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack disp :=
-  fun b bT & phant_id (Choice.class bT) b =>
+Definition pack :=
+  fun bT b & phant_id (Choice.class bT) b =>
   fun m => Pack disp (@Class T b m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base   : class_of >-> Choice.class_of.
-Coercion mixin  : class_of >-> mixin_of.
-Coercion sort   : type >-> Sortclass.
+Module Exports.
+Coercion base : class_of >-> Choice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
 Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
-
 Canonical eqType.
 Canonical choiceType.
-
 Notation porderType := type.
 Notation porderMixin := mixin_of.
 Notation POrderMixin := Mixin.
 Notation POrderType disp T m := (@pack T disp _ _ id m).
-
-Notation "[ 'porderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation "[ 'porderType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
   (at level 0, format "[ 'porderType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'porderType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'porderType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'porderType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'porderType' 'of' T ]" := [porderType of T for _]
   (at level 0, format "[ 'porderType'  'of'  T ]") : form_scope.
-Notation "[ 'porderType' 'of' T 'with' disp ]" := [porderType of T for _ with disp]
+Notation "[ 'porderType' 'of' T 'with' disp ]" :=
+  [porderType of T for _ with disp]
   (at level 0, format "[ 'porderType'  'of'  T  'with' disp ]") : form_scope.
 End Exports.
-End POrder.
 
+End POrder.
 Import POrder.Exports.
 Bind Scope cpo_sort with POrder.sort.
 
 Module Import POrderDef.
 Section Def.
 
-Variable (display : unit).
-Local Notation porderType := (porderType display).
+Variable (disp : unit).
+Local Notation porderType := (porderType disp).
 Variable (T : porderType).
 
 Definition le (R : porderType) : rel R := POrder.le (POrder.class R).
@@ -388,15 +426,15 @@ Definition leif (x y : T) C : Prop := ((x <= y) * ((x == y) = C))%type.
 
 Definition le_of_leif x y C (le_xy : @leif x y C) := le_xy.1 : le x y.
 
-CoInductive le_xor_gt (x y : T) : bool -> bool -> Set :=
+Variant le_xor_gt (x y : T) : bool -> bool -> Set :=
   | LerNotGt of x <= y : le_xor_gt x y true false
   | GtrNotLe of y < x  : le_xor_gt x y false true.
 
-CoInductive lt_xor_ge (x y : T) : bool -> bool -> Set :=
+Variant lt_xor_ge (x y : T) : bool -> bool -> Set :=
   | LtrNotGe of x < y  : lt_xor_ge x y false true
   | GerNotLt of y <= x : lt_xor_ge x y true false.
 
-CoInductive comparer (x y : T) :
+Variant comparer (x y : T) :
   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | ComparerEq of x = y : comparer x y
     true true true true false false
@@ -405,7 +443,7 @@ CoInductive comparer (x y : T) :
   | ComparerGt of y < x : comparer x y
     false false false true false true.
 
-CoInductive incomparer (x y : T) :
+Variant incomparer (x y : T) :
   bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | InComparerEq of x = y : incomparer x y
     true true true true false false true true
@@ -462,7 +500,7 @@ Notation "x <= y < z" := ((x <= y) && (y < z)) : order_scope.
 Notation "x < y < z" := ((x < y) && (y < z)) : order_scope.
 
 Notation "x <= y ?= 'iff' C" := (leif x y C) : order_scope.
-Notation "x <= y ?= 'iff' C :> R" := ((x : R) <= (y : R) ?= iff C)
+Notation "x <= y ?= 'iff' C :> T" := ((x : T) <= (y : T) ?= iff C)
   (only parsing) : order_scope.
 
 Notation ">=< x" := (comparable x) : order_scope.
@@ -473,14 +511,16 @@ 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.
 
-Coercion le_of_leif : leif >-> is_true.
-
 End POSyntax.
 
+Module POCoercions.
+Coercion le_of_leif : leif >-> is_true.
+End POCoercions.
+
 Module Lattice.
 Section ClassDef.
 
-Structure mixin_of d (T : porderType d) := Mixin {
+Record mixin_of d (T : porderType d) := Mixin {
   meet : T -> T -> T;
   join : T -> T -> T;
   _ : commutative meet;
@@ -493,72 +533,103 @@ Structure mixin_of d (T : porderType d) := Mixin {
   _ : left_distributive meet join;
 }.
 
-Record class_of d (T : Type) := Class {
+Record class_of (T : Type) := Class {
   base  : POrder.class_of T;
-  mixin : mixin_of (POrder.Pack d base)
+  mixin_disp : unit;
+  mixin : mixin_of (POrder.Pack mixin_disp base)
 }.
 
 Local Coercion base : class_of >-> POrder.class_of.
 
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
+Structure type (disp : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (@POrder.Pack disp T b0)) :=
   fun bT b & phant_id (@POrder.class disp bT) b =>
-    fun    m & phant_id m0 m => Pack (@Class disp T b m).
+  fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
 Definition porderType := @POrder.Pack disp cT xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> POrder.class_of.
-Coercion mixin     : class_of >-> mixin_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> POrder.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
 Coercion porderType : type >-> POrder.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
-
 Notation latticeType  := type.
 Notation latticeMixin := mixin_of.
 Notation LatticeMixin := Mixin.
-Notation LatticeType T m := (@pack T _ _ m _ _ id _ id).
-
-Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation LatticeType T m := (@pack T _ _ m _ _ id _ _ id).
+Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
   (at level 0, format "[ 'latticeType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'latticeType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'latticeType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'latticeType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'latticeType' 'of' T ]" := [latticeType of T for _]
   (at level 0, format "[ 'latticeType'  'of'  T ]") : form_scope.
-Notation "[ 'latticeType' 'of' T 'with' disp ]" := [latticeType of T for _ with disp]
+Notation "[ 'latticeType' 'of' T 'with' disp ]" :=
+  [latticeType of T for _ with disp]
   (at level 0, format "[ 'latticeType'  'of'  T  'with' disp ]") : form_scope.
 End Exports.
-End Lattice.
 
+End Lattice.
 Export Lattice.Exports.
 
 Module Import LatticeDef.
 Section LatticeDef.
-Context {display : unit}.
-Local Notation latticeType := (latticeType display).
-Definition meet {T : latticeType} : T -> T -> T := Lattice.meet (Lattice.class T).
-Definition join {T : latticeType} : T -> T -> T := Lattice.join (Lattice.class T).
+Context {disp : unit}.
+Local Notation latticeType := (latticeType disp).
+Context {T : latticeType}.
+Definition meet : T -> T -> T := Lattice.meet (Lattice.class T).
+Definition join : T -> T -> T := Lattice.join (Lattice.class T).
+
+Variant le_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
+  | LerNotGt of x <= y : le_xor_gt x y true false x x y y
+  | GtrNotLe of y < x  : le_xor_gt x y false true y y x x.
+
+Variant lt_xor_ge (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
+  | LtrNotGe of x < y  : lt_xor_ge x y false true x x y y
+  | GerNotLt of y <= x : lt_xor_ge x y true false y y x x.
+
+Variant comparer (x y : T) :
+  bool -> bool -> bool -> bool -> bool -> bool -> T -> T -> T -> T -> Set :=
+  | ComparerEq of x = y : comparer x y
+    true true true true false false x x x x
+  | ComparerLt of x < y : comparer x y
+    false false true false true false x x y y
+  | ComparerGt of y < x : comparer x y
+    false false false true false true y y x x.
+
+Variant incomparer (x y : T) :
+  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool ->
+  T -> T -> T -> T -> Set :=
+  | InComparerEq of x = y : incomparer x y
+    true true true true false false true true x x x x
+  | InComparerLt of x < y : incomparer x y
+    false false true false true false true true x x y y
+  | InComparerGt of y < x : incomparer x y
+    false false false true false true true true y y x x
+  | InComparer of x >< y  : incomparer x y
+    false false false false false false false false
+    (meet x y) (meet x y) (join x y) (join x y).
+
 End LatticeDef.
 End LatticeDef.
 
@@ -570,31 +641,32 @@ Notation "x `|` y" := (join x y).
 End LatticeSyntax.
 
 Module Total.
+Definition mixin_of d (T : latticeType d) := (total (<=%O : rel T)).
 Section ClassDef.
-Local Notation mixin_of T := (total (<=%O : rel T)).
 
-Record class_of d (T : Type) := Class {
-  base  : Lattice.class_of d T;
-  mixin : total (<=%O : rel (POrder.Pack d base))
+Record class_of (T : Type) := Class {
+  base  : Lattice.class_of T;
+  mixin_disp : unit;
+  mixin : mixin_of (Lattice.Pack mixin_disp base)
 }.
 
 Local Coercion base : class_of >-> Lattice.class_of.
 
-Structure type d := Pack { sort; _ : class_of d sort }.
+Structure type (d : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone disp' c & phant_id class c := @Pack disp' T c.
+Definition clone_with disp' c & phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (@Lattice.Pack disp T b0)) :=
   fun bT b & phant_id (@Lattice.class disp bT) b =>
-    fun    m & phant_id m0 m => Pack (@Class disp T b m).
+  fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -603,66 +675,140 @@ Definition latticeType := @Lattice.Pack disp cT xclass.
 
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> Lattice.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> Lattice.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
 Coercion porderType : type >-> POrder.type.
 Coercion latticeType : type >-> Lattice.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
 Canonical latticeType.
-
 Notation orderType  := type.
-Notation OrderType T m := (@pack T _ _ m _ _ id _ id).
-
-Notation "[ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation OrderType T m := (@pack T _ _ m _ _ id _ _ id).
+Notation "[ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ id)
   (at level 0, format "[ 'orderType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'orderType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'orderType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'orderType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'orderType' 'of' T ]" := [orderType of T for _]
   (at level 0, format "[ 'orderType'  'of'  T ]") : form_scope.
-Notation "[ 'orderType' 'of' T 'with' disp ]" := [orderType of T for _ with disp]
+Notation "[ 'orderType' 'of' T 'with' disp ]" :=
+  [orderType of T for _ with disp]
   (at level 0, format "[ 'orderType'  'of'  T  'with' disp ]") : form_scope.
-
 End Exports.
-End Total.
 
+End Total.
 Import Total.Exports.
 
+Module Import TotalDef.
+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.
+End TotalDef.
+
+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 min := (@meet total_display _).
+Notation "@ 'min' R" :=
+  (@meet total_display R) (at level 10, R at level 8, only parsing).
+
+Notation "\max_ ( i <- r | P ) F" :=
+  (\big[@join total_display _/0%O]_(i <- r | P%B) F%O) : order_scope.
+Notation "\max_ ( i <- r ) F" :=
+  (\big[@join total_display _/0%O]_(i <- r) F%O) : order_scope.
+Notation "\max_ ( i | P ) F" :=
+  (\big[@join total_display _/0%O]_(i | P%B) F%O) : order_scope.
+Notation "\max_ i F" :=
+  (\big[@join total_display _/0%O]_i F%O) : order_scope.
+Notation "\max_ ( i : I | P ) F" :=
+  (\big[@join total_display _/0%O]_(i : I | P%B) F%O) (only parsing) :
+  order_scope.
+Notation "\max_ ( i : I ) F" :=
+  (\big[@join total_display _/0%O]_(i : I) F%O) (only parsing) : order_scope.
+Notation "\max_ ( m <= i < n | P ) F" :=
+  (\big[@join total_display _/0%O]_(m <= i < n | P%B) F%O) : order_scope.
+Notation "\max_ ( m <= i < n ) F" :=
+  (\big[@join total_display _/0%O]_(m <= i < n) F%O) : order_scope.
+Notation "\max_ ( i < n | P ) F" :=
+  (\big[@join total_display _/0%O]_(i < n | P%B) F%O) : order_scope.
+Notation "\max_ ( i < n ) F" :=
+  (\big[@join total_display _/0%O]_(i < n) F%O) : order_scope.
+Notation "\max_ ( i 'in' A | P ) F" :=
+  (\big[@join total_display _/0%O]_(i in A | P%B) F%O) : order_scope.
+Notation "\max_ ( i 'in' A ) F" :=
+  (\big[@join total_display _/0%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.
+
 Module BLattice.
 Section ClassDef.
-Structure mixin_of d (T : porderType d) := Mixin {
+Record mixin_of d (T : porderType d) := Mixin {
   bottom : T;
   _ : forall x, bottom <= x;
 }.
 
-Record class_of d (T : Type) := Class {
-  base  : Lattice.class_of d T;
-  mixin : mixin_of (POrder.Pack d base)
+Record class_of (T : Type) := Class {
+  base  : Lattice.class_of T;
+  mixin_disp : unit;
+  mixin : mixin_of (POrder.Pack mixin_disp base)
 }.
 
 Local Coercion base : class_of >-> Lattice.class_of.
 
-Structure type d := Pack { sort; _ : class_of d sort}.
+Structure type (d : unit) := Pack { sort; _ : class_of sort}.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (@Lattice.Pack disp T b0)) :=
   fun bT b & phant_id (@Lattice.class disp bT) b =>
-    fun    m & phant_id m0 m => Pack (@Class disp T b m).
+  fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -670,37 +816,36 @@ Definition porderType := @POrder.Pack disp cT xclass.
 Definition latticeType := @Lattice.Pack disp cT xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> Lattice.class_of.
-Coercion mixin     : class_of >-> mixin_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> Lattice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
 Coercion porderType : type >-> POrder.type.
 Coercion latticeType : type >-> Lattice.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
 Canonical latticeType.
-
 Notation blatticeType  := type.
 Notation blatticeMixin := mixin_of.
 Notation BLatticeMixin := Mixin.
-Notation BLatticeType T m := (@pack T _ _ m _ _ id _ id).
-
-Notation "[ 'blatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation BLatticeType T m := (@pack T _ _ m _ _ id _ _ id).
+Notation "[ 'blatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
   (at level 0, format "[ 'blatticeType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'blatticeType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'blatticeType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'blatticeType' 'of' T ]" := [blatticeType of T for _]
   (at level 0, format "[ 'blatticeType'  'of'  T ]") : form_scope.
-Notation "[ 'blatticeType' 'of' T 'with' disp ]" := [blatticeType of T for _ with disp]
+Notation "[ 'blatticeType' 'of' T 'with' disp ]" :=
+  [blatticeType of T for _ with disp]
   (at level 0, format "[ 'blatticeType'  'of'  T  'with' disp ]") : form_scope.
 End Exports.
-End BLattice.
 
+End BLattice.
 Export BLattice.Exports.
 
 Module Import BLatticeDef.
@@ -724,49 +869,50 @@ Notation "\join_ ( i : I | P ) F" :=
 Notation "\join_ ( i : I ) F" :=
   (\big[@join _ _/0%O]_(i : I) F%O) (only parsing) : order_scope.
 Notation "\join_ ( m <= i < n | P ) F" :=
- (\big[@join _ _/0%O]_(m <= i < n | P%B) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(m <= i < n | P%B) F%O) : order_scope.
 Notation "\join_ ( m <= i < n ) F" :=
- (\big[@join _ _/0%O]_(m <= i < n) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(m <= i < n) F%O) : order_scope.
 Notation "\join_ ( i < n | P ) F" :=
- (\big[@join _ _/0%O]_(i < n | P%B) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(i < n | P%B) F%O) : order_scope.
 Notation "\join_ ( i < n ) F" :=
- (\big[@join _ _/0%O]_(i < n) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(i < n) F%O) : order_scope.
 Notation "\join_ ( i 'in' A | P ) F" :=
- (\big[@join _ _/0%O]_(i in A | P%B) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(i in A | P%B) F%O) : order_scope.
 Notation "\join_ ( i 'in' A ) F" :=
- (\big[@join _ _/0%O]_(i in A) F%O) : order_scope.
+  (\big[@join _ _/0%O]_(i in A) F%O) : order_scope.
 
 End BLatticeSyntax.
 
 Module TBLattice.
 Section ClassDef.
-Structure mixin_of d (T : porderType d) := Mixin {
+Record mixin_of d (T : porderType d) := Mixin {
   top : T;
   _ : forall x, x <= top;
 }.
 
-Record class_of d (T : Type) := Class {
-  base  : BLattice.class_of d T;
-  mixin : mixin_of (POrder.Pack d base)
+Record class_of (T : Type) := Class {
+  base  : BLattice.class_of T;
+  mixin_disp : unit;
+  mixin : mixin_of (POrder.Pack mixin_disp base)
 }.
 
 Local Coercion base : class_of >-> BLattice.class_of.
 
-Structure type d := Pack { sort; _ : class_of d sort }.
+Structure type (d : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (@BLattice.Pack disp T b0)) :=
   fun bT b & phant_id (@BLattice.class disp bT) b =>
-    fun    m & phant_id m0 m => Pack (@Class disp T b m).
+  fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -775,39 +921,37 @@ Definition latticeType := @Lattice.Pack disp cT xclass.
 Definition blatticeType := @BLattice.Pack disp cT xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> BLattice.class_of.
-Coercion mixin     : class_of >-> mixin_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> BLattice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion porderType : type >-> POrder.type.
 Coercion latticeType : type >-> Lattice.type.
 Coercion blatticeType : type >-> BLattice.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
 Canonical latticeType.
 Canonical blatticeType.
-
 Notation tblatticeType  := type.
 Notation tblatticeMixin := mixin_of.
 Notation TBLatticeMixin := Mixin.
-Notation TBLatticeType T m := (@pack T _ _ m _ _ id _ id).
-
-Notation "[ 'tblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation TBLatticeType T m := (@pack T _ _ m _ _ id _ _ id).
+Notation "[ 'tblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
   (at level 0, format "[ 'tblatticeType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'tblatticeType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'tblatticeType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'tblatticeType' 'of' T ]" := [tblatticeType of T for _]
   (at level 0, format "[ 'tblatticeType'  'of'  T ]") : form_scope.
-Notation "[ 'tblatticeType' 'of' T 'with' disp ]" := [tblatticeType of T for _ with disp]
+Notation "[ 'tblatticeType' 'of' T 'with' disp ]" :=
+  [tblatticeType of T for _ with disp]
   (at level 0, format "[ 'tblatticeType'  'of'  T  'with' disp ]") : form_scope.
-
 End Exports.
-End TBLattice.
 
+End TBLattice.
 Export TBLattice.Exports.
 
 Module Import TBLatticeDef.
@@ -848,34 +992,35 @@ End TBLatticeSyntax.
 
 Module CBLattice.
 Section ClassDef.
-Structure mixin_of d (T : blatticeType d) := Mixin {
+Record mixin_of d (T : blatticeType d) := Mixin {
   sub : T -> T -> T;
   _ : forall x y, y `&` sub x y = bottom;
   _ : forall x y, (x `&` y) `|` sub x y = x
 }.
 
-Record class_of d (T : Type) := Class {
-  base  : BLattice.class_of d T;
-  mixin : mixin_of (BLattice.Pack base)
+Record class_of (T : Type) := Class {
+  base  : BLattice.class_of T;
+  mixin_disp : unit;
+  mixin : mixin_of (BLattice.Pack mixin_disp base)
 }.
 
 Local Coercion base : class_of >-> BLattice.class_of.
 
-Structure type d := Pack { sort; _ : class_of d sort }.
+Structure type (d : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack b0 (m0 : mixin_of (@BLattice.Pack disp T b0)) :=
   fun bT b & phant_id (@BLattice.class disp bT) b =>
-    fun    m & phant_id m0 m => Pack (@Class disp T b m).
+  fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -884,40 +1029,38 @@ Definition latticeType := @Lattice.Pack disp cT xclass.
 Definition blatticeType := @BLattice.Pack disp cT xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> BLattice.class_of.
-Coercion mixin     : class_of >-> mixin_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> BLattice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
 Coercion porderType : type >-> POrder.type.
 Coercion latticeType : type >-> Lattice.type.
 Coercion blatticeType : type >-> BLattice.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
 Canonical latticeType.
 Canonical blatticeType.
-
 Notation cblatticeType  := type.
 Notation cblatticeMixin := mixin_of.
 Notation CBLatticeMixin := Mixin.
-Notation CBLatticeType T m := (@pack T _ _ m _ _ id _ id).
-
-Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
+Notation CBLatticeType T m := (@pack T _ _ m _ _ id _ _ id).
+Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
   (at level 0, format "[ 'cblatticeType'  'of'  T  'for'  cT ]") : form_scope.
 Notation "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'cblatticeType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'cblatticeType'  'of'  T  'for'  cT  'with'  disp ]") :
+  form_scope.
 Notation "[ 'cblatticeType' 'of' T ]" := [cblatticeType of T for _]
   (at level 0, format "[ 'cblatticeType'  'of'  T ]") : form_scope.
-Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := [cblatticeType of T for _ with disp]
+Notation "[ 'cblatticeType' 'of' T 'with' disp ]" :=
+  [cblatticeType of T for _ with disp]
   (at level 0, format "[ 'cblatticeType'  'of'  T  'with' disp ]") : form_scope.
-
 End Exports.
-End CBLattice.
 
+End CBLattice.
 Export CBLattice.Exports.
 
 Module Import CBLatticeDef.
@@ -936,35 +1079,35 @@ Record mixin_of d (T : tblatticeType d) (sub : T -> T -> T) := Mixin {
    _ : forall x, compl x = sub top x
 }.
 
-Record class_of d (T : Type) := Class {
-  base  : TBLattice.class_of d T;
-  mixin1 : CBLattice.mixin_of (BLattice.Pack base);
-  mixin2 : @mixin_of d (TBLattice.Pack base) (CBLattice.sub mixin1)
+Record class_of (T : Type) := Class {
+  base  : TBLattice.class_of T;
+  mixin1_disp : unit;
+  mixin1 : CBLattice.mixin_of (BLattice.Pack mixin1_disp base);
+  mixin2_disp : unit;
+  mixin2 : @mixin_of _ (TBLattice.Pack mixin2_disp base) (CBLattice.sub mixin1)
 }.
 
 Local Coercion base : class_of >-> TBLattice.class_of.
-Local Coercion base2 d T (c : class_of d T) :=
+Local Coercion base2 T (c : class_of T) : CBLattice.class_of T :=
   CBLattice.Class (mixin1 c).
 
-Structure type d := Pack { sort; _ : class_of d sort }.
+Structure type (d : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Definition clone disp' c of (disp = disp') & phant_id class c :=
-  @Pack disp' T c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack disp T c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
 Definition pack :=
-  fun bT b & phant_id (@TBLattice.class disp bT)
-                      (b : TBLattice.class_of disp T) =>
-  fun m1T m1 &  phant_id (@CBLattice.class disp m1T)
-                         (@CBLattice.Class disp T b m1) =>
-  fun (m2 : @mixin_of disp (@TBLattice.Pack disp T b) (CBLattice.sub m1)) =>
-  Pack (@Class disp T b m1 m2).
+  fun bT  b  & phant_id (@TBLattice.class disp bT) b =>
+  fun disp1 m1T m1 & phant_id (@CBLattice.class disp1 m1T)
+                              (@CBLattice.Class _ _ _ m1) =>
+  fun disp2 m2 => Pack disp (@Class T b disp1 m1 disp2 m2).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -977,20 +1120,19 @@ Definition tbd_cblatticeType :=
   @CBLattice.Pack disp tblatticeType xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> TBLattice.class_of.
-Coercion base2     : class_of >-> CBLattice.class_of.
-Coercion mixin1     : class_of >-> CBLattice.mixin_of.
-Coercion mixin2     : class_of >-> mixin_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
+Module Exports.
+Coercion base : class_of >-> TBLattice.class_of.
+Coercion base2 : class_of >-> CBLattice.class_of.
+Coercion mixin1 : class_of >-> CBLattice.mixin_of.
+Coercion mixin2 : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
 Coercion porderType : type >-> POrder.type.
 Coercion latticeType : type >-> Lattice.type.
 Coercion blatticeType : type >-> BLattice.type.
 Coercion tblatticeType : type >-> TBLattice.type.
 Coercion cblatticeType : type >-> CBLattice.type.
-
 Canonical eqType.
 Canonical choiceType.
 Canonical porderType.
@@ -999,29 +1141,28 @@ Canonical blatticeType.
 Canonical tblatticeType.
 Canonical cblatticeType.
 Canonical tbd_cblatticeType.
-
 Notation ctblatticeType  := type.
 Notation ctblatticeMixin := mixin_of.
 Notation CTBLatticeMixin := Mixin.
-Notation CTBLatticeType T m := (@pack T _ _ _ id _ _ id m).
-
-Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id)
-  (at level 0, format "[ 'cblatticeType'  'of'  T  'for'  cT ]") : form_scope.
-Notation "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]" :=
-  (@clone T _ cT disp _ (unit_irrelevance _ _) id)
-  (at level 0, format "[ 'cblatticeType'  'of'  T  'for'  cT  'with'  disp ]") : form_scope.
-Notation "[ 'cblatticeType' 'of' T ]" := [cblatticeType of T for _]
-  (at level 0, format "[ 'cblatticeType'  'of'  T ]") : form_scope.
-Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := [cblatticeType of T for _ with disp]
-  (at level 0, format "[ 'cblatticeType'  'of'  T  'with' disp ]") : form_scope.
-
+Notation CTBLatticeType T m := (@pack T _ _ _ id _ _ _ id _ m).
+Notation "[ 'ctblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
+  (at level 0, format "[ 'ctblatticeType'  'of'  T  'for'  cT ]") : form_scope.
+Notation "[ 'ctblatticeType' 'of' T 'for' cT 'with' disp ]" :=
+  (@clone_with T _ cT disp _ id)
+  (at level 0, format "[ 'ctblatticeType'  'of'  T  'for'  cT  'with'  disp ]")
+  : form_scope.
+Notation "[ 'ctblatticeType' 'of' T ]" := [ctblatticeType of T for _]
+  (at level 0, format "[ 'ctblatticeType'  'of'  T ]") : form_scope.
+Notation "[ 'ctblatticeType' 'of' T 'with' disp ]" :=
+  [ctblatticeType of T for _ with disp]
+  (at level 0, format "[ 'ctblatticeType'  'of'  T  'with' disp ]") :
+  form_scope.
 Notation "[ 'default_ctblatticeType' 'of' T ]" :=
-  (@pack T _ _ _ id _ _ id (fun=> erefl))
+  (@pack T _ _ _ id _ _ id (Mixin (fun=> erefl)))
   (at level 0, format "[ 'default_ctblatticeType'  'of'  T ]") : form_scope.
-
 End Exports.
-End CTBLattice.
 
+End CTBLattice.
 Export CTBLattice.Exports.
 
 Module Import CTBLatticeDef.
@@ -1041,13 +1182,13 @@ Module FinPOrder.
 Section ClassDef.
 
 Record class_of T := Class {
-  base  : Finite.class_of T;
-  mixin : POrder.mixin_of (Equality.Pack base)
+  base  : POrder.class_of T;
+  mixin : Finite.mixin_of (Equality.Pack base)
 }.
 
-Local Coercion base : class_of >-> Finite.class_of.
-Definition base2 T (c : class_of T) := (POrder.Class (mixin c)).
-Local Coercion base2 : class_of >-> POrder.class_of.
+Local Coercion base : class_of >-> POrder.class_of.
+Local Coercion base2 T (c : class_of T) : Finite.class_of T :=
+  Finite.Class (mixin c).
 
 Structure type (disp : unit) := Pack { sort; _ : class_of sort }.
 
@@ -1060,580 +1201,386 @@ Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 
 Definition pack :=
-  fun b bT & phant_id (Finite.class bT) b =>
-  fun m mT & phant_id (POrder.mixin_of mT) m =>
+  fun bT b & phant_id (@POrder.class disp bT) b =>
+  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
   Pack disp (@Class T b m).
 
 Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT xclass.
+Definition finType := @Finite.Pack cT xclass.
 Definition porderType := @POrder.Pack disp cT xclass.
+Definition count_porderType := @POrder.Pack disp countType xclass.
 Definition fin_porderType := @POrder.Pack disp finType xclass.
 End ClassDef.
 
-Module Import Exports.
-Coercion base   : class_of >-> Finite.class_of.
-Coercion base2  : class_of >-> POrder.class_of.
-Coercion sort   : type >-> Sortclass.
+Module Exports.
+Coercion base : class_of >-> POrder.class_of.
+Coercion base2 : class_of >-> Finite.class_of.
+Coercion sort : type >-> Sortclass.
 Coercion eqType : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
 Coercion choiceType : type >-> Choice.type.
+Coercion countType : type >-> Countable.type.
+Coercion finType : type >-> Finite.type.
 Coercion porderType : type >-> POrder.type.
-
 Canonical eqType.
-Canonical finType.
 Canonical choiceType.
+Canonical countType.
+Canonical finType.
 Canonical porderType.
+Canonical count_porderType.
 Canonical fin_porderType.
-
 Notation finPOrderType := type.
-Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
+Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
   (at level 0, format "[ 'finPOrderType'  'of'  T ]") : form_scope.
-
 End Exports.
-End FinPOrder.
 
+End FinPOrder.
 Import FinPOrder.Exports.
 Bind Scope cpo_sort with FinPOrder.sort.
 
 Module FinLattice.
 Section ClassDef.
 
-Record class_of d (T : Type) := Class {
-  base  : FinPOrder.class_of T;
-  mixin : Lattice.mixin_of (POrder.Pack d base)
+Record class_of (T : Type) := Class {
+  base : TBLattice.class_of T;
+  mixin : Finite.mixin_of (Equality.Pack base);
 }.
 
-Local Coercion base : class_of >-> FinPOrder.class_of.
-Definition base2 d T (c : class_of d T) := (Lattice.Class (mixin c)).
-Local Coercion base2 : class_of >-> Lattice.class_of.
-
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
-
-Local Coercion sort : type >-> Sortclass.
-
-Variables (T : Type) (disp : unit) (cT : type disp).
-
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
-
-Definition pack disp :=
-  fun bT b & phant_id (@FinPOrder.class disp bT) b =>
-  fun mT m & phant_id (@Lattice.mixin disp mT) m =>
-  Pack (@Class disp T b m).
-
-Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition fin_latticeType := @Lattice.Pack disp finPOrderType xclass.
-
-End ClassDef.
-
-Module Import Exports.
-Coercion base      : class_of >-> FinPOrder.class_of.
-Coercion base2     : class_of >-> Lattice.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
-Coercion choiceType : type >-> Choice.type.
-Coercion porderType : type >-> POrder.type.
-Coercion finPOrderType : type >-> FinPOrder.type.
-Coercion latticeType : type >-> Lattice.type.
-
-Canonical eqType.
-Canonical finType.
-Canonical choiceType.
-Canonical porderType.
-Canonical finPOrderType.
-Canonical latticeType.
-Canonical fin_latticeType.
-
-Notation finLatticeType  := type.
-
-Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
-  (at level 0, format "[ 'finLatticeType'  'of'  T ]") : form_scope.
-End Exports.
-End FinLattice.
-
-Export FinLattice.Exports.
-
-Module FinTotal.
-Section ClassDef.
-
-Record class_of d (T : Type) := Class {
-  base  : FinLattice.class_of d T;
-  mixin : total (<=%O : rel (POrder.Pack d base))
-}.
-
-Local Coercion base : class_of >-> FinLattice.class_of.
-Definition base2 d T (c : class_of d T) :=
-   (@Total.Class _ _ (FinLattice.base2 c) (@mixin _ _ c)).
-Local Coercion base2 : class_of >-> Total.class_of.
-
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
-
-Local Coercion sort : type >-> Sortclass.
-
-Variables (T : Type) (disp : unit) (cT : type disp).
-
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
-
-Definition pack disp :=
-  fun bT b & phant_id (@FinPOrder.class disp bT) b =>
-  fun mT m & phant_id (@Total.mixin disp mT) m =>
-  Pack (@Class disp T b m).
-
-Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
-Definition orderType := @Total.Pack disp cT xclass.
-Definition fin_orderType := @Total.Pack disp finLatticeType xclass.
-
-End ClassDef.
-
-Module Import Exports.
-Coercion base      : class_of >-> FinLattice.class_of.
-Coercion base2     : class_of >-> Total.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
-Coercion choiceType : type >-> Choice.type.
-Coercion porderType : type >-> POrder.type.
-Coercion finPOrderType : type >-> FinPOrder.type.
-Coercion latticeType : type >-> Lattice.type.
-Coercion finLatticeType : type >-> FinLattice.type.
-Coercion orderType : type >-> Total.type.
-
-Canonical eqType.
-Canonical finType.
-Canonical choiceType.
-Canonical porderType.
-Canonical finPOrderType.
-Canonical latticeType.
-Canonical finLatticeType.
-Canonical orderType.
-Canonical fin_orderType.
-
-Notation finOrderType  := type.
-
-Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
-  (at level 0, format "[ 'finOrderType'  'of'  T ]") : form_scope.
-End Exports.
-End FinTotal.
-
-Export Total.Exports.
-
-Module FinBLattice.
-Section ClassDef.
-
-Record class_of d (T : Type) := Class {
-  base  : FinLattice.class_of d T;
-  mixin : BLattice.mixin_of (FinPOrder.Pack d base)
-}.
-
-Local Coercion base : class_of >-> FinLattice.class_of.
-Definition base2 d T (c : class_of d T) :=
-   (@BLattice.Class _ _ (FinLattice.base2 c) (@mixin _ _ c)).
-Local Coercion base2 : class_of >-> BLattice.class_of.
+Local Coercion base : class_of >-> TBLattice.class_of.
+Local Coercion base2 T (c : class_of T) : Finite.class_of T :=
+  Finite.Class (mixin c).
+Local Coercion base3 T (c : class_of T) : FinPOrder.class_of T :=
+  @FinPOrder.Class T c c.
 
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
+Structure type (disp : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
-Definition pack disp :=
-  fun bT b & phant_id (@FinPOrder.class disp bT) b =>
-  fun mT m & phant_id (@BLattice.mixin disp mT) m =>
-  Pack (@Class disp T b m).
+Definition pack :=
+  fun bT b & phant_id (@TBLattice.class disp bT) b =>
+  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
+  Pack disp (@Class T b m).
 
 Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
-Definition porderType := @POrder.Pack disp cT xclass.
-Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
-Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
-Definition blatticeType := @BLattice.Pack disp cT xclass.
-Definition fin_blatticeType := @BLattice.Pack disp finLatticeType xclass.
-
-End ClassDef.
-
-Module Import Exports.
-Coercion base      : class_of >-> FinLattice.class_of.
-Coercion base2     : class_of >-> BLattice.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
-Coercion choiceType : type >-> Choice.type.
-Coercion porderType : type >-> POrder.type.
-Coercion finPOrderType : type >-> FinPOrder.type.
-Coercion latticeType : type >-> Lattice.type.
-Coercion finLatticeType : type >-> FinLattice.type.
-Coercion blatticeType : type >-> BLattice.type.
-
-Canonical eqType.
-Canonical finType.
-Canonical choiceType.
-Canonical porderType.
-Canonical finPOrderType.
-Canonical latticeType.
-Canonical finLatticeType.
-Canonical blatticeType.
-Canonical fin_blatticeType.
-
-Notation finBLatticeType  := type.
-
-Notation "[ 'finBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
-  (at level 0, format "[ 'finBLatticeType'  'of'  T ]") : form_scope.
-End Exports.
-End FinBLattice.
-
-Export FinBLattice.Exports.
-
-Module FinTBLattice.
-Section ClassDef.
-
-Record class_of d (T : Type) := Class {
-  base  : FinBLattice.class_of d T;
-  mixin : TBLattice.mixin_of (FinPOrder.Pack d base)
-}.
-
-Local Coercion base : class_of >-> FinBLattice.class_of.
-Definition base2 d T (c : class_of d T) :=
-   (@TBLattice.Class _ _ c (@mixin _ _ c)).
-Local Coercion base2 : class_of >-> TBLattice.class_of.
-
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
-
-Local Coercion sort : type >-> Sortclass.
-
-Variables (T : Type) (disp : unit) (cT : type disp).
-
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
-
-Definition pack disp :=
-  fun bT b & phant_id (@FinBLattice.class disp bT) b =>
-  fun mT m & phant_id (@TBLattice.mixin disp mT) m =>
-  Pack (@Class disp T b m).
-
-Definition eqType := @Equality.Pack cT xclass.
+Definition countType := @Countable.Pack cT xclass.
 Definition finType := @Finite.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
 Definition porderType := @POrder.Pack disp cT xclass.
 Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
 Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
 Definition blatticeType := @BLattice.Pack disp cT xclass.
-Definition finBLatticeType := @FinBLattice.Pack disp cT xclass.
 Definition tblatticeType := @TBLattice.Pack disp cT xclass.
-Definition fin_blatticeType := @TBLattice.Pack disp finBLatticeType xclass.
+Definition count_latticeType := @Lattice.Pack disp countType xclass.
+Definition count_blatticeType := @BLattice.Pack disp countType xclass.
+Definition count_tblatticeType := @TBLattice.Pack disp countType xclass.
+Definition fin_latticeType := @Lattice.Pack disp finType xclass.
+Definition fin_blatticeType := @BLattice.Pack disp finType xclass.
+Definition fin_tblatticeType := @TBLattice.Pack disp finType xclass.
+Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass.
+Definition finPOrder_blatticeType := @BLattice.Pack disp finPOrderType xclass.
+Definition finPOrder_tblatticeType := @TBLattice.Pack disp finPOrderType xclass.
 
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> FinBLattice.class_of.
-Coercion base2     : class_of >-> TBLattice.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
+Module Exports.
+Coercion base : class_of >-> TBLattice.class_of.
+Coercion base2 : class_of >-> Finite.class_of.
+Coercion base3 : class_of >-> FinPOrder.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
+Coercion countType : type >-> Countable.type.
+Coercion finType : type >-> Finite.type.
 Coercion porderType : type >-> POrder.type.
 Coercion finPOrderType : type >-> FinPOrder.type.
 Coercion latticeType : type >-> Lattice.type.
-Coercion finLatticeType : type >-> FinLattice.type.
 Coercion blatticeType : type >-> BLattice.type.
-Coercion finBLatticeType : type >-> FinBLattice.type.
 Coercion tblatticeType : type >-> TBLattice.type.
-
 Canonical eqType.
-Canonical finType.
 Canonical choiceType.
+Canonical countType.
+Canonical finType.
 Canonical porderType.
 Canonical finPOrderType.
 Canonical latticeType.
-Canonical finLatticeType.
 Canonical blatticeType.
-Canonical finBLatticeType.
 Canonical tblatticeType.
+Canonical count_latticeType.
+Canonical count_blatticeType.
+Canonical count_tblatticeType.
+Canonical fin_latticeType.
 Canonical fin_blatticeType.
-
-Notation finTBLatticeType  := type.
-
-Notation "[ 'finTBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
-  (at level 0, format "[ 'finTBLatticeType'  'of'  T ]") : form_scope.
+Canonical fin_tblatticeType.
+Canonical finPOrder_latticeType.
+Canonical finPOrder_blatticeType.
+Canonical finPOrder_tblatticeType.
+Notation finLatticeType  := type.
+Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
+  (at level 0, format "[ 'finLatticeType'  'of'  T ]") : form_scope.
 End Exports.
-End FinTBLattice.
 
-Export FinTBLattice.Exports.
+End FinLattice.
+Export FinLattice.Exports.
 
-Module FinCBLattice.
+Module FinCLattice.
 Section ClassDef.
 
-Record class_of d (T : Type) := Class {
-  base  : FinBLattice.class_of d T;
-  mixin : CBLattice.mixin_of (BLattice.Pack base)
+Record class_of (T : Type) := Class {
+  base  : CTBLattice.class_of T;
+  mixin : Finite.mixin_of (Equality.Pack base);
 }.
 
-Local Coercion base : class_of >-> FinBLattice.class_of.
-Definition base2 d T (c : class_of d T) :=
-   (@CBLattice.Class _ _ c (@mixin _ _ c)).
-Local Coercion base2 : class_of >-> CBLattice.class_of.
+Local Coercion base : class_of >-> CTBLattice.class_of.
+Local Coercion base2 T (c : class_of T) : Finite.class_of T :=
+  Finite.Class (mixin c).
+Local Coercion base3 T (c : class_of T) : FinLattice.class_of T :=
+  @FinLattice.Class T c c.
 
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
+Structure type (disp : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
-Definition pack disp :=
-  fun bT b & phant_id (@FinBLattice.class disp bT) b =>
-  fun mT m & phant_id (@CBLattice.mixin disp mT) m =>
-  Pack (@Class disp T b m).
+Definition pack :=
+  fun bT b & phant_id (@CTBLattice.class disp bT) b =>
+  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) =>
+  Pack disp (@Class T b m).
 
 Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT xclass.
+Definition finType := @Finite.Pack cT xclass.
 Definition porderType := @POrder.Pack disp cT xclass.
 Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
 Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
 Definition blatticeType := @BLattice.Pack disp cT xclass.
-Definition finBLatticeType := @FinBLattice.Pack disp cT xclass.
+Definition tblatticeType := @TBLattice.Pack disp cT xclass.
+Definition finLatticeType := @FinLattice.Pack disp cT xclass.
 Definition cblatticeType := @CBLattice.Pack disp cT xclass.
-Definition fin_blatticeType := @CBLattice.Pack disp finBLatticeType xclass.
+Definition ctblatticeType := @CTBLattice.Pack disp cT xclass.
+Definition count_cblatticeType := @CBLattice.Pack disp countType xclass.
+Definition count_ctblatticeType := @CTBLattice.Pack disp countType xclass.
+Definition fin_cblatticeType := @CBLattice.Pack disp finType xclass.
+Definition fin_ctblatticeType := @CTBLattice.Pack disp finType xclass.
+Definition finPOrder_cblatticeType := @CBLattice.Pack disp finPOrderType xclass.
+Definition finPOrder_ctblatticeType :=
+  @CTBLattice.Pack disp finPOrderType xclass.
+Definition finLattice_cblatticeType :=
+  @CBLattice.Pack disp finLatticeType xclass.
+Definition finLattice_ctblatticeType :=
+  @CTBLattice.Pack disp finLatticeType xclass.
 
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> FinBLattice.class_of.
-Coercion base2     : class_of >-> CBLattice.class_of.
-Coercion sort      : type >-> Sortclass.
-Coercion eqType    : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
+Module Exports.
+Coercion base : class_of >-> CTBLattice.class_of.
+Coercion base2 : class_of >-> Finite.class_of.
+Coercion base3 : class_of >-> FinLattice.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
 Coercion choiceType : type >-> Choice.type.
+Coercion countType : type >-> Countable.type.
+Coercion finType : type >-> Finite.type.
 Coercion porderType : type >-> POrder.type.
 Coercion finPOrderType : type >-> FinPOrder.type.
 Coercion latticeType : type >-> Lattice.type.
-Coercion finLatticeType : type >-> FinLattice.type.
 Coercion blatticeType : type >-> BLattice.type.
-Coercion finBLatticeType : type >-> FinBLattice.type.
+Coercion tblatticeType : type >-> TBLattice.type.
+Coercion finLatticeType : type >-> FinLattice.type.
 Coercion cblatticeType : type >-> CBLattice.type.
-
+Coercion ctblatticeType : type >-> CTBLattice.type.
 Canonical eqType.
-Canonical finType.
 Canonical choiceType.
+Canonical countType.
+Canonical finType.
 Canonical porderType.
 Canonical finPOrderType.
 Canonical latticeType.
-Canonical finLatticeType.
 Canonical blatticeType.
-Canonical finBLatticeType.
+Canonical tblatticeType.
+Canonical finLatticeType.
 Canonical cblatticeType.
-Canonical fin_blatticeType.
-
-Notation finCBLatticeType  := type.
-
-Notation "[ 'finCBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
-  (at level 0, format "[ 'finCBLatticeType'  'of'  T ]") : form_scope.
+Canonical ctblatticeType.
+Canonical count_cblatticeType.
+Canonical count_ctblatticeType.
+Canonical fin_cblatticeType.
+Canonical fin_ctblatticeType.
+Canonical finPOrder_cblatticeType.
+Canonical finPOrder_ctblatticeType.
+Canonical finLattice_cblatticeType.
+Canonical finLattice_ctblatticeType.
+Notation finCLatticeType  := type.
+Notation "[ 'finCLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
+  (at level 0, format "[ 'finCLatticeType'  'of'  T ]") : form_scope.
 End Exports.
-End FinCBLattice.
 
-Export FinCBLattice.Exports.
+End FinCLattice.
+Export FinCLattice.Exports.
 
-Module FinCTBLattice.
+Module FinTotal.
 Section ClassDef.
 
-Record class_of d (T : Type) := Class {
-  base  : FinTBLattice.class_of d T;
-  mixin1 : CBLattice.mixin_of (BLattice.Pack base);
-  mixin2 : @CTBLattice.mixin_of d (TBLattice.Pack base) (CBLattice.sub mixin1)
+Record class_of (T : Type) := Class {
+  base  : FinLattice.class_of T;
+  mixin_disp : unit;
+  mixin : Total.mixin_of (Lattice.Pack mixin_disp base)
 }.
 
-Local Coercion base : class_of >-> FinTBLattice.class_of.
-Definition base1 d T (c : class_of d T) :=
-   (@FinCBLattice.Class _ _ c (@mixin1 _ _ c)).
-Local Coercion base1 : class_of >-> FinCBLattice.class_of.
-Definition base2 d T (c : class_of d T) :=
-   (@CTBLattice.Class _ _ c (@mixin1 _ _ c) (@mixin2 _ _ c)).
-Local Coercion base2 : class_of >-> CTBLattice.class_of.
+Local Coercion base : class_of >-> FinLattice.class_of.
+Local Coercion base2 T (c : class_of T) : Total.class_of T :=
+  @Total.Class _ c _ (mixin (c := c)).
 
-Structure type (display : unit) :=
-  Pack { sort; _ : class_of display sort }.
+Structure type (disp : unit) := Pack { sort; _ : class_of sort }.
 
 Local Coercion sort : type >-> Sortclass.
 
 Variables (T : Type) (disp : unit) (cT : type disp).
 
-Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c.
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
 Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of _ xT).
+Notation xclass := (class : class_of xT).
 
-Definition pack disp :=
-  fun bT b & phant_id (@FinTBLattice.class disp bT) b =>
-  fun m1T m1 & phant_id (@CTBLattice.mixin1 disp m1T) m1 =>
-  fun m2T m2 & phant_id (@CTBLattice.mixin2 disp m2T) m2 =>
-  Pack (@Class disp T b m1 m2).
+Definition pack :=
+  fun bT b & phant_id (@FinLattice.class disp bT) b =>
+  fun disp' mT m & phant_id (@Total.class disp mT) (@Total.Class _ _ _ m) =>
+  Pack disp (@Class T b disp' m).
 
 Definition eqType := @Equality.Pack cT xclass.
-Definition finType := @Finite.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
+Definition countType := @Countable.Pack cT xclass.
+Definition finType := @Finite.Pack cT xclass.
 Definition porderType := @POrder.Pack disp cT xclass.
 Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
 Definition latticeType := @Lattice.Pack disp cT xclass.
-Definition finLatticeType := @FinLattice.Pack disp cT xclass.
 Definition blatticeType := @BLattice.Pack disp cT xclass.
-Definition finBLatticeType := @FinBLattice.Pack disp cT xclass.
-Definition cblatticeType := @CBLattice.Pack disp cT xclass.
 Definition tblatticeType := @TBLattice.Pack disp cT xclass.
-Definition finTBLatticeType := @FinTBLattice.Pack disp cT xclass.
-Definition finCBLatticeType := @FinCBLattice.Pack disp cT xclass.
-Definition ctblatticeType := @CTBLattice.Pack disp cT xclass.
-Definition fintb_ctblatticeType := @CTBLattice.Pack disp finTBLatticeType xclass.
-Definition fincb_ctblatticeType := @CTBLattice.Pack disp finCBLatticeType xclass.
+Definition finLatticeType := @FinLattice.Pack disp cT xclass.
+Definition orderType := @Total.Pack disp cT xclass.
+Definition order_countType := @Countable.Pack orderType xclass.
+Definition order_finType := @Finite.Pack orderType xclass.
+Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass.
+Definition order_blatticeType := @BLattice.Pack disp orderType xclass.
+Definition order_tblatticeType := @TBLattice.Pack disp orderType xclass.
+Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass.
 
 End ClassDef.
 
-Module Import Exports.
-Coercion base      : class_of >-> FinTBLattice.class_of.
-Coercion base1     : class_of >-> FinCBLattice.class_of.
-Coercion base2     : class_of >-> CTBLattice.class_of.
-Coercion sort      : type >-> Sortclass.
-
+Module Exports.
+Coercion base : class_of >-> FinLattice.class_of.
+Coercion base2 : class_of >-> Total.class_of.
+Coercion sort : type >-> Sortclass.
 Coercion eqType : type >-> Equality.type.
-Coercion finType : type >-> Finite.type.
 Coercion choiceType : type >-> Choice.type.
+Coercion countType : type >-> Countable.type.
+Coercion finType : type >-> Finite.type.
 Coercion porderType : type >-> POrder.type.
 Coercion finPOrderType : type >-> FinPOrder.type.
 Coercion latticeType : type >-> Lattice.type.
-Coercion finLatticeType : type >-> FinLattice.type.
 Coercion blatticeType : type >-> BLattice.type.
-Coercion finBLatticeType : type >-> FinBLattice.type.
-Coercion cblatticeType : type >-> CBLattice.type.
 Coercion tblatticeType : type >-> TBLattice.type.
-Coercion finTBLatticeType : type >-> FinTBLattice.type.
-Coercion finCBLatticeType : type >-> FinCBLattice.type.
-Coercion ctblatticeType : type >-> CTBLattice.type.
-Coercion fintb_ctblatticeType : type >-> CTBLattice.type.
-Coercion fincb_ctblatticeType : type >-> CTBLattice.type.
-
-
+Coercion finLatticeType : type >-> FinLattice.type.
+Coercion orderType : type >-> Total.type.
 Canonical eqType.
-Canonical finType.
 Canonical choiceType.
+Canonical countType.
+Canonical finType.
 Canonical porderType.
 Canonical finPOrderType.
 Canonical latticeType.
-Canonical finLatticeType.
 Canonical blatticeType.
-Canonical finBLatticeType.
-Canonical cblatticeType.
 Canonical tblatticeType.
-Canonical finTBLatticeType.
-Canonical finCBLatticeType.
-Canonical ctblatticeType.
-Canonical fintb_ctblatticeType.
-Canonical fincb_ctblatticeType.
-
-Notation finCTBLatticeType  := type.
-
-Notation "[ 'finCTBLatticeType' 'of' T ]" :=
-  (@pack T _ _ erefl _ _ phant_id  _ _ phant_id _ _ phant_id)
-  (at level 0, format "[ 'finCTBLatticeType'  'of'  T ]") : form_scope.
+Canonical finLatticeType.
+Canonical orderType.
+Canonical order_countType.
+Canonical order_finType.
+Canonical order_finPOrderType.
+Canonical order_blatticeType.
+Canonical order_tblatticeType.
+Canonical order_finLatticeType.
+Notation finOrderType := type.
+Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ _ id)
+  (at level 0, format "[ 'finOrderType'  'of'  T ]") : form_scope.
 End Exports.
-End FinCTBLattice.
 
-Export FinCTBLattice.Exports.
+End FinTotal.
+Export Total.Exports.
 
-(***********)
-(* REVERSE *)
-(***********)
+(************)
+(* CONVERSE *)
+(************)
 
-Definition reverse T : Type := T.
-Definition reverse_display : unit -> unit. Proof. exact. Qed.
-Local Notation "T ^r" := (reverse T) (at level 2, format "T ^r") : type_scope.
+Definition converse T : Type := T.
+Definition converse_display : unit -> unit. Proof. exact. Qed.
+Local Notation "T ^c" := (converse T) (at level 2, format "T ^c") : type_scope.
 
-Module Import ReverseSyntax.
+Module Import ConverseSyntax.
 
-Notation "<=^r%O" := (@le (reverse_display _) _) : order_scope.
-Notation ">=^r%O" := (@ge (reverse_display _) _)  : order_scope.
-Notation ">=^r%O" := (@ge (reverse_display _) _)  : order_scope.
-Notation "<^r%O" := (@lt (reverse_display _) _) : order_scope.
-Notation ">^r%O" := (@gt (reverse_display _) _) : order_scope.
-Notation "<?=^r%O" := (@leif (reverse_display _) _) : order_scope.
-Notation ">=<^r%O" := (@comparable (reverse_display _) _) : order_scope.
-Notation "><^r%O" := (fun x y => ~~ (@comparable (reverse_display _) _ x y)) :
+Notation "<=^c%O" := (@le (converse_display _) _) : order_scope.
+Notation ">=^c%O" := (@ge (converse_display _) _)  : order_scope.
+Notation ">=^c%O" := (@ge (converse_display _) _)  : order_scope.
+Notation "<^c%O" := (@lt (converse_display _) _) : order_scope.
+Notation ">^c%O" := (@gt (converse_display _) _) : order_scope.
+Notation "<?=^c%O" := (@leif (converse_display _) _) : order_scope.
+Notation ">=<^c%O" := (@comparable (converse_display _) _) : order_scope.
+Notation "><^c%O" := (fun x y => ~~ (@comparable (converse_display _) _ x y)) :
   order_scope.
 
-Notation "<=^r y" := (>=^r%O y) : order_scope.
-Notation "<=^r y :> T" := (<=^r (y : T)) : order_scope.
-Notation ">=^r y"  := (<=^r%O y) : order_scope.
-Notation ">=^r y :> T" := (>=^r (y : T)) : order_scope.
+Notation "<=^c y" := (>=^c%O y) : order_scope.
+Notation "<=^c y :> T" := (<=^c (y : T)) : order_scope.
+Notation ">=^c y"  := (<=^c%O y) : order_scope.
+Notation ">=^c y :> T" := (>=^c (y : T)) : order_scope.
 
-Notation "<^r y" := (>^r%O y) : order_scope.
-Notation "<^r y :> T" := (<^r (y : T)) : order_scope.
-Notation ">^r y" := (<^r%O y) : order_scope.
-Notation ">^r y :> T" := (>^r (y : T)) : order_scope.
+Notation "<^c y" := (>^c%O y) : order_scope.
+Notation "<^c y :> T" := (<^c (y : T)) : order_scope.
+Notation ">^c y" := (<^c%O y) : order_scope.
+Notation ">^c y :> T" := (>^c (y : T)) : order_scope.
 
-Notation ">=<^r y" := (>=<^r%O y) : order_scope.
-Notation ">=<^r y :> T" := (>=<^r (y : T)) : order_scope.
+Notation ">=<^c y" := (>=<^c%O y) : order_scope.
+Notation ">=<^c y :> T" := (>=<^c (y : T)) : order_scope.
 
-Notation "x <=^r y" := (<=^r%O x y) : order_scope.
-Notation "x <=^r y :> T" := ((x : T) <=^r (y : T)) : order_scope.
-Notation "x >=^r y" := (y <=^r x) (only parsing) : order_scope.
-Notation "x >=^r y :> T" := ((x : T) >=^r (y : T)) (only parsing) : order_scope.
+Notation "x <=^c y" := (<=^c%O x y) : order_scope.
+Notation "x <=^c y :> T" := ((x : T) <=^c (y : T)) : order_scope.
+Notation "x >=^c y" := (y <=^c x) (only parsing) : order_scope.
+Notation "x >=^c y :> T" := ((x : T) >=^c (y : T)) (only parsing) : order_scope.
 
-Notation "x <^r y"  := (<^r%O x y) : order_scope.
-Notation "x <^r y :> T" := ((x : T) <^r (y : T)) : order_scope.
-Notation "x >^r y"  := (y <^r x) (only parsing) : order_scope.
-Notation "x >^r y :> T" := ((x : T) >^r (y : T)) (only parsing) : order_scope.
+Notation "x <^c y"  := (<^c%O x y) : order_scope.
+Notation "x <^c y :> T" := ((x : T) <^c (y : T)) : order_scope.
+Notation "x >^c y"  := (y <^c x) (only parsing) : order_scope.
+Notation "x >^c y :> T" := ((x : T) >^c (y : T)) (only parsing) : order_scope.
 
-Notation "x <=^r y <=^r z" := ((x <=^r y) && (y <=^r z)) : order_scope.
-Notation "x <^r y <=^r z" := ((x <^r y) && (y <=^r z)) : order_scope.
-Notation "x <=^r y <^r z" := ((x <=^r y) && (y <^r z)) : order_scope.
-Notation "x <^r y <^r z" := ((x <^r y) && (y <^r z)) : order_scope.
+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 <^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 <=^r y ?= 'iff' C" := (<?=^r%O x y C) : order_scope.
-Notation "x <=^r y ?= 'iff' C :> R" := ((x : R) <=^r (y : R) ?= iff C)
+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)
   (only parsing) : order_scope.
 
-Notation ">=<^r x" := (>=<^r%O x) : order_scope.
-Notation ">=<^r x :> T" := (>=<^r (x : T)) (only parsing) : order_scope.
-Notation "x >=<^r y" := (>=<^r%O x y) : order_scope.
+Notation ">=<^c x" := (>=<^c%O x) : order_scope.
+Notation ">=<^c x :> T" := (>=<^c (x : T)) (only parsing) : order_scope.
+Notation "x >=<^c y" := (>=<^c%O x y) : order_scope.
 
-Notation "><^r x" := (fun y => ~~ (>=<^r%O x y)) : order_scope.
-Notation "><^r x :> T" := (><^r (x : T)) (only parsing) : order_scope.
-Notation "x ><^r y" := (~~ (><^r%O x y)) : order_scope.
+Notation "><^c x" := (fun y => ~~ (>=<^c%O x y)) : order_scope.
+Notation "><^c x :> T" := (><^c (x : T)) (only parsing) : order_scope.
+Notation "x ><^c y" := (~~ (><^c%O x y)) : order_scope.
 
-Notation "x `&^r` y" :=  (@meet (reverse_display _) _ x y).
-Notation "x `|^r` y" := (@join (reverse_display _) _ x y).
+Notation "x `&^c` y" :=  (@meet (converse_display _) _ x y).
+Notation "x `|^c` y" := (@join (converse_display _) _ x y).
 
-End ReverseSyntax.
+End ConverseSyntax.
 
 (**********)
 (* THEORY *)
@@ -1641,34 +1588,50 @@ End ReverseSyntax.
 
 Module Import POrderTheory.
 Section POrderTheory.
+Import POrderDef.
 
-Context {display : unit}.
-Local Notation porderType := (porderType display).
+Context {disp : unit}.
+Local Notation porderType := (porderType disp).
 Context {T : porderType}.
 
 Implicit Types x y : 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.
+
 Lemma lexx (x : T) : x <= x.
 Proof. by case: T x => ? [? []]. Qed.
-Hint Resolve lexx.
+Hint Resolve lexx : core.
 
 Definition le_refl : reflexive le := lexx.
-Hint Resolve le_refl.
+Definition ge_refl : reflexive ge := lexx.
+Hint Resolve le_refl : core.
 
 Lemma le_anti: antisymmetric (<=%O : rel T).
 Proof. by case: T => ? [? []]. Qed.
 
+Lemma ge_anti: antisymmetric (>=%O : rel T).
+Proof. by move=> x y /le_anti. Qed.
+
 Lemma le_trans: transitive (<=%O : rel T).
 Proof. by case: T => ? [? []]. Qed.
 
-Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y).
+Lemma ge_trans: transitive (>=%O : rel T).
+Proof. by move=> ? ? ? ? /le_trans; apply. Qed.
+
+Lemma lt_def x y: (x < y) = (y != x) && (x <= y).
 Proof. by case: T x y => ? [? []]. Qed.
 
+Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y).
+Proof. by rewrite lt_def eq_sym. Qed.
+
 Lemma ltxx x: x < x = false.
-Proof. by rewrite lt_neqAle eqxx. Qed.
+Proof. by rewrite lt_def eqxx. Qed.
 
 Definition lt_irreflexive : irreflexive lt := ltxx.
-Hint Resolve lt_irreflexive.
+Hint Resolve lt_irreflexive : core.
+
+Definition ltexx := (lexx, ltxx).
 
 Lemma le_eqVlt x y: (x <= y) = (x == y) || (x < y).
 Proof. by rewrite lt_neqAle; case: eqP => //= ->; rewrite lexx. Qed.
@@ -1700,6 +1663,9 @@ Proof. by rewrite le_eqVlt => /orP [/eqP ->|/lt_trans t /t]. Qed.
 Lemma lt_nsym x y : x < y -> y < x -> False.
 Proof. by move=> xy /(lt_trans xy); rewrite ltxx. Qed.
 
+Lemma lt_asym x y : x < y < x = false.
+Proof. by apply/negP => /andP []; apply: lt_nsym. Qed.
+
 Lemma le_gtF x y: x <= y -> y < x = false.
 Proof.
 by move=> le_xy; apply/negP => /lt_le_trans /(_ le_xy); rewrite ltxx.
@@ -1719,11 +1685,13 @@ by rewrite lt_neqAle lexy andbT; apply: contraNneq Nleyx => ->.
 Qed.
 
 Lemma lt_le_asym x y : x < y <= x = false.
-Proof. by rewrite lt_neqAle -andbA -eq_le eq_sym; case: (_ == _). Qed.
+Proof. by rewrite lt_neqAle -andbA -eq_le eq_sym andNb. Qed.
 
 Lemma le_lt_asym x y : x <= y < x = false.
 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.
 Proof.
@@ -1818,58 +1786,183 @@ rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]].
 by move=> /orP[/eqP->|lxy] <-; rewrite ?eqxx // lt_eqF.
 Qed.
 
+Lemma leif_refl x C : reflect (x <= x ?= iff C) C.
+Proof. by apply: (iffP idP) => [-> | <-] //; split; rewrite ?eqxx. Qed.
+
+Lemma leif_trans x1 x2 x3 C12 C23 :
+  x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23.
+Proof.
+move=> ltx12 ltx23; apply/leifP; rewrite -ltx12.
+case eqx12: (x1 == x2).
+  by rewrite (eqP eqx12) lt_neqAle !ltx23 andbT; case C23.
+by rewrite (@lt_le_trans x2) ?ltx23 // lt_neqAle eqx12 ltx12.
+Qed.
+
+Lemma leif_le x y : x <= y -> x <= y ?= iff (x >= y).
+Proof. by move=> lexy; split=> //; rewrite eq_le lexy. Qed.
+
+Lemma leif_eq x y : x <= y -> x <= y ?= iff (x == y).
+Proof. by []. Qed.
+
+Lemma ge_leif x y C : x <= y ?= iff C -> (y <= x) = C.
+Proof. by case=> le_xy; rewrite eq_le le_xy. Qed.
+
+Lemma lt_leif x y C : x <= y ?= iff C -> (x < y) = ~~ C.
+Proof. by move=> le_xy; rewrite lt_neqAle !le_xy andbT. Qed.
+
+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)}.
+Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed.
+
+Lemma mono_leif (f : T -> T) C :
+    {mono f : x y / x <= y} ->
+  forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).
+Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
+
+Lemma nmono_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) = (y <= x ?= iff C)}.
+Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed.
+
+Lemma nmono_leif (f : T -> T) C :
+    {mono f : x y /~ x <= y} ->
+  forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C).
+Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
+
 End POrderTheory.
+Section POrderMonotonyTheory.
+
+Context {disp disp' : unit}.
+Context {T : porderType disp} {T' : porderType disp'}.
+Implicit Types (m n p : nat) (x y z : T) (u v w : T').
+Variables (D D' : {pred T}) (f : T -> T').
+
+Hint Resolve lexx lt_neqAle (@le_anti _ T) (@le_anti _ T') lt_def : core.
+
+Let ge_antiT : antisymmetric (>=%O : rel T).
+Proof. by move=> ? ? /le_anti. Qed.
+
+Lemma ltW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}.
+Proof. exact: homoW. Qed.
+
+Lemma ltW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y}.
+Proof. exact: homoW. Qed.
+
+Lemma inj_homo_lt :
+  injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y}.
+Proof. exact: inj_homo. Qed.
+
+Lemma inj_nhomo_lt :
+  injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y}.
+Proof. exact: inj_homo. Qed.
+
+Lemma inc_inj : {mono f : x y / x <= y} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma dec_inj : {mono f : x y /~ x <= y} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma leW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y}.
+Proof. exact: anti_mono. Qed.
+
+Lemma leW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y}.
+Proof. exact: anti_mono. Qed.
+
+(* Monotony in D D' *)
+Lemma ltW_homo_in :
+  {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma ltW_nhomo_in :
+  {in D & D', {homo f : x y /~ x < y}} -> {in D & D', {homo f : x y /~ x <= y}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma inj_homo_lt_in :
+    {in D & D', injective f} ->  {in D & D', {homo f : x y / x <= y}} ->
+  {in D & D', {homo f : x y / x < y}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma inj_nhomo_lt_in :
+    {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} ->
+  {in D & D', {homo f : x y /~ x < y}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma inc_inj_in : {in D &, {mono f : x y / x <= y}} ->
+   {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma dec_inj_in :
+  {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma leW_mono_in :
+  {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma leW_nmono_in :
+  {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}}.
+Proof. exact: anti_mono_in. Qed.
+
+End POrderMonotonyTheory.
+
 End POrderTheory.
 
-Hint Resolve lexx le_refl lt_irreflexive.
+Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core.
 
+Arguments leifP {disp T x y C}.
+Arguments leif_refl {disp T x C}.
+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].
 
-Module Import ReversePOrder.
-Section ReversePOrder.
-Canonical reverse_eqType (T : eqType) := EqType T [eqMixin of T^r].
-Canonical reverse_choiceType (T : choiceType) := [choiceType of T^r].
+Module Import ConversePOrder.
+Section ConversePOrder.
+Canonical converse_eqType (T : eqType) := EqType T [eqMixin of T^c].
+Canonical converse_choiceType (T : choiceType) := [choiceType of T^c].
 
-Context {display : unit}.
-Local Notation porderType := (porderType display).
+Context {disp : unit}.
+Local Notation porderType := (porderType disp).
 Variable T : porderType.
 
-Definition reverse_le (x y : T) := (y <= x).
-Definition reverse_lt (x y : T) := (y < x).
+Definition converse_le (x y : T) := (y <= x).
+Definition converse_lt (x y : T) := (y < x).
 
-Lemma reverse_lt_neqAle (x y : T) : reverse_lt x y = (x != y) && (reverse_le x y).
-Proof. by rewrite eq_sym; apply: lt_neqAle. Qed.
+Lemma converse_lt_def (x y : T) :
+  converse_lt x y = (y != x) && (converse_le x y).
+Proof. by apply: lt_neqAle. Qed.
 
-Fact reverse_le_anti : antisymmetric reverse_le.
+Fact converse_le_anti : antisymmetric converse_le.
 Proof. by move=> x y /andP [xy yx]; apply/le_anti/andP; split. Qed.
 
-Definition reverse_porderMixin :=
-  POrderMixin reverse_lt_neqAle (lexx : reflexive reverse_le) reverse_le_anti
+Definition converse_porderMixin :=
+  POrderMixin converse_lt_def (lexx : reflexive converse_le) converse_le_anti
              (fun y z x zy yx => @le_trans _ _ y x z yx zy).
-Canonical reverse_porderType :=
-  POrderType (reverse_display display) (T^r) reverse_porderMixin.
+Canonical converse_porderType :=
+  POrderType (converse_display disp) (T^c) converse_porderMixin.
 
-End ReversePOrder.
-End ReversePOrder.
+End ConversePOrder.
+End ConversePOrder.
 
-Definition LePOrderMixin T le rle ale tle :=
-   @POrderMixin T le _ (fun _ _ => erefl) rle ale tle.
-
-Module Import ReverseLattice.
-Section ReverseLattice.
-Context {display : unit}.
-Local Notation latticeType := (latticeType display).
+Module Import ConverseLattice.
+Section ConverseLattice.
+Context {disp : unit}.
+Local Notation latticeType := (latticeType disp).
 
 Variable L : latticeType.
 Implicit Types (x y : L).
 
-Lemma meetC : commutative (@meet _ L). Proof. by case: L => [?[?[]]]. Qed.
-Lemma joinC : commutative (@join _ L). Proof. by case: L => [?[?[]]]. Qed.
+Lemma meetC : commutative (@meet _ L). Proof. by case: L => [?[? ?[]]]. Qed.
+Lemma joinC : commutative (@join _ L). Proof. by case: L => [?[? ?[]]]. Qed.
 
-Lemma meetA : associative (@meet _ L). Proof. by case: L => [?[?[]]]. Qed.
-Lemma joinA : associative (@join _ L). Proof. by case: L => [?[?[]]]. Qed.
+Lemma meetA : associative (@meet _ L). Proof. by case: L => [?[? ?[]]]. Qed.
+Lemma joinA : associative (@join _ L). Proof. by case: L => [?[? ?[]]]. Qed.
 
-Lemma joinKI y x : x `&` (x `|` y) = x. Proof. by case: L x y => [?[?[]]]. Qed.
-Lemma meetKU y x : x `|` (x `&` y) = x. Proof. by case: L x y => [?[?[]]]. Qed.
+Lemma joinKI y x : x `&` (x `|` y) = x.
+Proof. by case: L x y => [?[? ?[]]]. Qed.
+Lemma meetKU y x : x `|` (x `&` y) = x.
+Proof. by case: L x y => [?[? ?[]]]. Qed.
 
 Lemma joinKIC y x : x `&` (y `|` x) = x. Proof. by rewrite joinC joinKI. Qed.
 Lemma meetKUC y x : x `|` (y `&` x) = x. Proof. by rewrite meetC meetKU. Qed.
@@ -1883,13 +1976,13 @@ Lemma meetUKC x y : (y `&` x) `|` y = y. Proof. by rewrite meetC meetUK. Qed.
 Lemma joinIKC x y : (y `|` x) `&` y = y. Proof. by rewrite joinC joinIK. Qed.
 
 Lemma leEmeet x y : (x <= y) = (x `&` y == x).
-Proof. by case: L x y => [?[?[]]]. Qed.
+Proof. by case: L x y => [?[? ?[]]]. Qed.
 
 Lemma leEjoin x y : (x <= y) = (x `|` y == y).
 Proof. by rewrite leEmeet; apply/eqP/eqP => <-; rewrite (joinKI, meetUK). Qed.
 
 Lemma meetUl : left_distributive (@meet _ L) (@join _ L).
-Proof. by case: L => [?[?[]]]. Qed.
+Proof. by case: L => [?[? ?[]]]. Qed.
 
 Lemma meetUr : right_distributive (@meet _ L) (@join _ L).
 Proof. by move=> x y z; rewrite meetC meetUl ![_ `&` x]meetC. Qed.
@@ -1897,20 +1990,20 @@ Proof. by move=> x y z; rewrite meetC meetUl ![_ `&` x]meetC. Qed.
 Lemma joinIl : left_distributive (@join _ L) (@meet _ L).
 Proof. by move=> x y z; rewrite meetUr joinIK meetUl -joinA meetUKC. Qed.
 
-Fact reverse_leEmeet (x y : L^r) : (x <= y) = (x `|` y == x).
+Fact converse_leEmeet (x y : L^c) : (x <= y) = (x `|` y == x).
 Proof. by rewrite [LHS]leEjoin joinC. Qed.
 
-Definition reverse_latticeMixin :=
-   @LatticeMixin _ [porderType of L^r] _ _ joinC meetC
-  joinA meetA meetKU joinKI reverse_leEmeet joinIl.
-Canonical reverse_latticeType := LatticeType L^r reverse_latticeMixin.
-End ReverseLattice.
-End ReverseLattice.
+Definition converse_latticeMixin :=
+   @LatticeMixin _ [porderType of L^c] _ _ joinC meetC
+  joinA meetA meetKU joinKI converse_leEmeet joinIl.
+Canonical converse_latticeType := LatticeType L^c converse_latticeMixin.
+End ConverseLattice.
+End ConverseLattice.
 
 Module Import LatticeTheoryMeet.
 Section LatticeTheoryMeet.
-Context {display : unit}.
-Local Notation latticeType := (latticeType display).
+Context {disp : unit}.
+Local Notation latticeType := (latticeType disp).
 Context {L : latticeType}.
 Implicit Types (x y : L).
 
@@ -1936,16 +2029,6 @@ Proof. by rewrite meetAC meetC meetxx. Qed.
 
 (* interaction with order *)
 
-Lemma meet_idPl {x y} : reflect (x `&` y = x) (x <= y).
-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 leIidl x y : (x <= x `&` y) = (x <= y).
-Proof. by rewrite !leEmeet meetKI. Qed.
-Lemma leIidr x y : (x <= y `&` x) = (x <= y).
-Proof. by rewrite !leEmeet meetKIC. Qed.
-
 Lemma lexI x y z : (x <= y `&` z) = (x <= y) && (x <= z).
 Proof.
 rewrite !leEmeet; apply/idP/idP => [/eqP<-|/andP[/eqP<- /eqP<-]].
@@ -1953,192 +2036,295 @@ rewrite !leEmeet; apply/idP/idP => [/eqP<-|/andP[/eqP<- /eqP<-]].
 by rewrite -[X in X `&` _]meetA meetIK meetA.
 Qed.
 
-Lemma leIx x y z : (y <= x) || (z <= x) -> y `&` z <= x.
-Proof.
-rewrite !leEmeet => /orP [/eqP <-|/eqP <-].
-  by rewrite -meetA meetACA meetxx meetAC.
-by rewrite -meetA meetIK.
-Qed.
+Lemma leIxl x y z : y <= x -> y `&` z <= x.
+Proof. by rewrite !leEmeet meetAC => /eqP ->. Qed.
+
+Lemma leIxr x y z : z <= x -> y `&` z <= x.
+Proof. by rewrite !leEmeet -meetA => /eqP ->. Qed.
+
+Lemma leIx2 x y z : (y <= x) || (z <= x) -> y `&` z <= x.
+Proof. by case/orP => [/leIxl|/leIxr]. Qed.
 
 Lemma leIr x y : y `&` x <= x.
-Proof. by rewrite leIx ?lexx ?orbT. Qed.
+Proof. by rewrite leIx2 ?lexx ?orbT. Qed.
 
 Lemma leIl x y : x `&` y <= x.
-Proof. by rewrite leIx ?lexx ?orbT. Qed.
+Proof. by rewrite leIx2 ?lexx ?orbT. Qed.
+
+Lemma meet_idPl {x y} : reflect (x `&` y = x) (x <= y).
+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 leIidl x y : (x <= x `&` y) = (x <= y).
+Proof. by rewrite !leEmeet meetKI. Qed.
+Lemma leIidr x y : (x <= y `&` x) = (x <= y).
+Proof. by rewrite !leEmeet meetKIC. Qed.
+
+Lemma eq_meetl x y : (x `&` y == x) = (x <= y).
+Proof. by apply/esym/leEmeet. Qed.
+
+Lemma eq_meetr x y : (x `&` y == y) = (y <= x).
+Proof. by rewrite meetC eq_meetl. Qed.
 
 Lemma leI2 x y z t : x <= z -> y <= t -> x `&` y <= z `&` t.
-Proof. by move=> xz yt; rewrite lexI !leIx ?xz ?yt ?orbT //. Qed.
+Proof. by move=> xz yt; rewrite lexI !leIx2 ?xz ?yt ?orbT //. Qed.
 
 End LatticeTheoryMeet.
 End LatticeTheoryMeet.
 
 Module Import LatticeTheoryJoin.
 Section LatticeTheoryJoin.
-Context {display : unit}.
-Local Notation latticeType := (latticeType display).
+Import LatticeDef.
+Context {disp : unit}.
+Local Notation latticeType := (latticeType disp).
 Context {L : latticeType}.
 Implicit Types (x y : L).
 
 (* lattice theory *)
 Lemma joinAC : right_commutative (@join _ L).
-Proof. exact: (@meetAC _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetAC _ [latticeType of L^c]). Qed.
 Lemma joinCA : left_commutative (@join _ L).
-Proof. exact: (@meetCA _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetCA _ [latticeType of L^c]). Qed.
 Lemma joinACA : interchange (@join _ L) (@join _ L).
-Proof. exact: (@meetACA _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetACA _ [latticeType of L^c]). Qed.
 
 Lemma joinxx x : x `|` x = x.
-Proof. exact: (@meetxx _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetxx _ [latticeType of L^c]). Qed.
 
 Lemma joinKU y x : x `|` (x `|` y) = x `|` y.
-Proof. exact: (@meetKI _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetKI _ [latticeType of L^c]). Qed.
 Lemma joinUK y x : (x `|` y) `|` y = x `|` y.
-Proof. exact: (@meetIK _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetIK _ [latticeType of L^c]). Qed.
 Lemma joinKUC y x : x `|` (y `|` x) = x `|` y.
-Proof. exact: (@meetKIC _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetKIC _ [latticeType of L^c]). Qed.
 Lemma joinUKC y x : y `|` x `|` y = x `|` y.
-Proof. exact: (@meetIKC _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetIKC _ [latticeType of L^c]). Qed.
 
 (* interaction with order *)
+Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z).
+Proof. exact: (@lexI _ [latticeType of L^c]). Qed.
+Lemma lexUl x y z : x <= y -> x <= y `|` z.
+Proof. exact: (@leIxl _ [latticeType of L^c]). Qed.
+Lemma lexUr x y z : x <= z -> x <= y `|` z.
+Proof. exact: (@leIxr _ [latticeType of L^c]). Qed.
+Lemma lexU2 x y z : (x <= y) || (x <= z) -> x <= y `|` z.
+Proof. exact: (@leIx2 _ [latticeType of L^c]). Qed.
+
+Lemma leUr x y : x <= y `|` x.
+Proof. exact: (@leIr _ [latticeType of L^c]). Qed.
+Lemma leUl x y : x <= x `|` y.
+Proof. exact: (@leIl _ [latticeType of L^c]). Qed.
+
 Lemma join_idPl {x y} : reflect (x `|` y = y) (x <= y).
-Proof. exact: (@meet_idPr _ [latticeType of L^r]). Qed.
+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^r]). Qed.
+Proof. exact: (@meet_idPl _ [latticeType of L^c]). Qed.
 
 Lemma leUidl x y : (x `|` y <= y) = (x <= y).
-Proof. exact: (@leIidr _ [latticeType of L^r]). Qed.
+Proof. exact: (@leIidr _ [latticeType of L^c]). Qed.
 Lemma leUidr x y : (y `|` x <= y) = (x <= y).
-Proof. exact: (@leIidl _ [latticeType of L^r]). Qed.
-
-Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z).
-Proof. exact: (@lexI _ [latticeType of L^r]). Qed.
+Proof. exact: (@leIidl _ [latticeType of L^c]). Qed.
 
-Lemma lexU x y z : (x <= y) || (x <= z) -> x <= y `|` z.
-Proof. exact: (@leIx _ [latticeType of L^r]). Qed.
-
-Lemma leUr x y : x <= y `|` x.
-Proof. exact: (@leIr _ [latticeType of L^r]). Qed.
-
-Lemma leUl x y : x <= x `|` y.
-Proof. exact: (@leIl _ [latticeType of L^r]). Qed.
+Lemma eq_joinl x y : (x `|` y == x) = (y <= x).
+Proof. exact: (@eq_meetl _ [latticeType of L^c]). Qed.
+Lemma eq_joinr x y : (x `|` y == y) = (x <= y).
+Proof. exact: (@eq_meetr _ [latticeType of L^c]). Qed.
 
 Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.
-Proof. exact: (@leI2 _ [latticeType of L^r]). Qed.
+Proof. exact: (@leI2 _ [latticeType of L^c]). Qed.
 
 (* Distributive lattice theory *)
 Lemma joinIr : right_distributive (@join _ L) (@meet _ L).
-Proof. exact: (@meetUr _ [latticeType of L^r]). Qed.
+Proof. exact: (@meetUr _ [latticeType of L^c]). Qed.
+
+Lemma lcomparableP x y : incomparer x y
+  (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y)
+  (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+Proof.
+by case: (comparableP x) => [-> | hxy | hxy | hxy]; do 1?have hxy' := ltW hxy;
+  rewrite ?(meetxx, joinxx, meetC y, joinC y)
+          ?(meet_idPl hxy', meet_idPr hxy', join_idPl hxy', join_idPr hxy');
+  constructor.
+Qed.
+
+Lemma lcomparable_ltgtP x y : x >=< y ->
+  comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y)
+           (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+Proof. by case: (lcomparableP x) => // *; constructor. Qed.
+
+Lemma lcomparable_leP x y : x >=< y ->
+  le_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+Proof. by move/lcomparable_ltgtP => [->|/ltW xy|xy]; constructor => //. Qed.
+
+Lemma lcomparable_ltP x y : x >=< y ->
+  lt_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+Proof. by move=> /lcomparable_ltgtP [->|xy|/ltW xy]; constructor => //. Qed.
 
 End LatticeTheoryJoin.
 End LatticeTheoryJoin.
 
-Module TotalLattice.
-Section TotalLattice.
-Context {display : unit}.
-Local Notation porderType := (porderType display).
-Context {T : porderType}.
-Implicit Types (x y z : T).
-Hypothesis le_total : total (<=%O : rel T).
+Module Import TotalTheory.
+Section TotalTheory.
+Context {disp : unit}.
+Local Notation orderType := (orderType disp).
+Context {T : orderType}.
+Implicit Types (x y z t : T).
 
-Fact comparableT x y : x >=< y. Proof. exact: le_total. Qed.
-Hint Resolve comparableT.
+Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed.
+Hint Resolve le_total : core.
 
-Fact ltgtP x y :
-  comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y).
-Proof. exact: comparable_ltgtP. Qed.
+Lemma ge_total : total (>=%O : rel T).
+Proof. by move=> ? ?; apply: le_total. Qed.
+Hint Resolve ge_total : core.
 
-Fact leP x y : le_xor_gt x y (x <= y) (y < x).
-Proof. exact: comparable_leP. Qed.
+Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed.
+Hint Resolve comparableT : core.
 
-Fact ltP x y : lt_xor_ge x y (y <= x) (x < y).
-Proof. exact: comparable_ltP. Qed.
+Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s).
+Proof. exact: sort_sorted. Qed.
 
-Definition meet x y := if x <= y then x else y.
-Definition join x y := if y <= x then x else y.
+Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s.
+Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed.
 
-Fact meetC : commutative meet.
-Proof. by move=> x y; rewrite /meet; have [] := ltgtP. Qed.
+Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s.
+Proof.
+by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort.
+Qed.
 
-Fact joinC : commutative join.
-Proof. by move=> x y; rewrite /join; have [] := ltgtP. Qed.
+Lemma leNgt x y : (x <= y) = ~~ (y < x). Proof. exact: comparable_leNgt. Qed.
 
-Fact meetA : associative meet.
+Lemma ltNge x y : (x < y) = ~~ (y <= x). Proof. exact: comparable_ltNge. Qed.
+
+Lemma wlog_le P :
+     (forall x y, P y x -> P x y) -> (forall x y, x <= y -> P x y) ->
+   forall x y, P x y.
 Proof.
-move=> x y z; rewrite /meet; case: (leP y z) => yz; case: (leP x y) => xy //=.
-- by rewrite (le_trans xy).
-- by rewrite yz.
-by rewrite !lt_geF // (lt_trans yz).
+move=> sP hP x y; case hxy: (x <= y); last apply/sP; apply/hP => //.
+by move/negbT: hxy; rewrite -ltNge; apply/ltW.
 Qed.
 
-Fact joinA : associative join.
+Lemma wlog_lt P :
+    (forall x, P x x) ->
+    (forall x y, (P y x -> P x y)) -> (forall x y, x < y -> P x y) ->
+  forall x y, P x y.
 Proof.
-move=> x y z; rewrite /join; case: (leP z y) => yz; case: (leP y x) => xy //=.
-- by rewrite (le_trans yz).
-- by rewrite yz.
-by rewrite !lt_geF // (lt_trans xy).
+move=> rP sP hP x y; case hxy: (x < y); first by apply/hP.
+case hxy': (x == y); first by move/eqP: hxy' => <-; apply: rP.
+by apply/sP/hP; rewrite lt_def leNgt hxy hxy'.
 Qed.
 
-Fact joinKI y x : meet x (join x y) = x.
-Proof. by rewrite /meet /join; case: (leP y x) => yx; rewrite ?lexx ?ltW. Qed.
+Definition ltgtP x y := LatticeTheoryJoin.lcomparable_ltgtP (comparableT x y).
+Definition leP x y := LatticeTheoryJoin.lcomparable_leP (comparableT x y).
+Definition ltP x y := LatticeTheoryJoin.lcomparable_ltP (comparableT x y).
 
-Fact meetKU y x : join x (meet x y) = x.
-Proof. by rewrite /meet /join; case: (leP x y) => yx; rewrite ?lexx ?ltW. Qed.
+Lemma neq_lt x y : (x != y) = (x < y) || (y < x). Proof. by case: ltgtP. Qed.
 
-Fact leEmeet x y : (x <= y) = (meet x y == x).
-Proof. by rewrite /meet; case: leP => ?; rewrite ?eqxx ?lt_eqF. Qed.
+Lemma lt_total x y : x != y -> (x < y) || (y < x). Proof. by case: ltgtP. Qed.
 
-Fact meetUl : left_distributive meet join.
+Lemma eq_leLR x y z t :
+  (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t).
+Proof. by move=> *; apply/idP/idP; rewrite // !leNgt; apply: contra. Qed.
+
+Lemma eq_leRL x y z t :
+  (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y).
+Proof. by move=> *; symmetry; apply: eq_leLR. Qed.
+
+Lemma eq_ltLR x y z t :
+  (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t).
+Proof. by move=> *; rewrite !ltNge; congr negb; apply: eq_leLR. Qed.
+
+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 *)
+
+Lemma leIx x y z : (meet y z <= x) = (y <= x) || (z <= x).
 Proof.
-move=> x y z; rewrite /meet /join.
-case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last.
-- by rewrite yz [x <= z](le_trans _ yz) ?[x <= y]ltW // lt_geF.
-- by rewrite lt_geF ?lexx // (lt_le_trans yz).
-- by rewrite lt_geF //; have [->|/lt_geF->|] := (ltgtP x z); rewrite ?lexx.
-- by have [] := (leP x z); rewrite ?xy ?yz.
+by case: (leP y z) => hyz; case: leP => ?;
+  rewrite ?(orbT, orbF) //=; apply/esym/negbTE;
+  rewrite -ltNge ?(lt_le_trans _ hyz) ?(lt_trans _ hyz).
 Qed.
 
-Definition Mixin := LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+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.
 
-End TotalLattice.
-End TotalLattice.
+Lemma ltxI x y z : (x < meet y z) = (x < y) && (x < z).
+Proof. by rewrite !ltNge leIx negb_or. Qed.
 
-Module TotalTheory.
-Section TotalTheory.
-Context {display : unit}.
-Local Notation orderType := (orderType display).
-Context {T : orderType}.
-Implicit Types (x y : T).
+Lemma ltIx x y z : (meet y z < x) = (y < x) || (z < x).
+Proof. by rewrite !ltNge lexI negb_and. Qed.
 
-Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed.
-Hint Resolve le_total.
+Lemma ltxU x y z : (x < join y z) = (x < y) || (x < z).
+Proof. by rewrite !ltNge leUx negb_and. Qed.
 
-Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed.
-Hint Resolve comparableT.
+Lemma ltUx x y z : (join y z < x) = (y < x) && (z < x).
+Proof. by rewrite !ltNge lexU negb_or. Qed.
 
-Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s).
-Proof. exact: sort_sorted. Qed.
+Definition ltexI := (@lexI _ T, ltxI).
+Definition lteIx := (leIx, ltIx).
+Definition ltexU := (lexU, ltxU).
+Definition lteUx := (@leUx _ T, ltUx).
 
-Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s.
-Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed.
+Section ArgExtremum.
 
-Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s.
+Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).
+
+Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F).
+Proof. by apply: extremumP => //; apply: le_trans. Qed.
+
+Lemma arg_maxP: extremum_spec >=%O P F (arg_max i0 P F).
+Proof. by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed.
+
+End ArgExtremum.
+
+End TotalTheory.
+Section TotalMonotonyTheory.
+
+Context {disp : unit} {disp' : unit}.
+Context {T : orderType disp} {T' : porderType disp'}.
+Variables (D : {pred T}) (f : T -> T').
+Implicit Types (x y z : T) (u v w : T').
+
+Lemma le_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}.
 Proof.
-by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort.
+move=> mf x y; case: ltgtP; first (by move=> ->; apply/lexx); move/mf => fxy.
+- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT.
+- by apply/ltW.
 Qed.
 
-Lemma leNgt x y : (x <= y) = ~~ (y < x).
-Proof. by rewrite comparable_leNgt. Qed.
+Lemma le_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}.
+Proof.
+move=> mf x y; case: ltgtP; first (by move=> ->; apply/lexx); move/mf => fxy.
+- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT.
+- by apply/ltW.
+Qed.
 
-Lemma ltNge x y : (x < y) = ~~ (y <= x).
-Proof. by rewrite comparable_ltNge. Qed.
+Lemma le_mono_in :
+  {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}}.
+Proof.
+move=> mf x y Dx Dy; case: ltgtP;
+  first (by move=> ->; apply/lexx); move/mf => fxy.
+- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT.
+- by apply/ltW/fxy.
+Qed.
 
-Definition ltgtP := TotalLattice.ltgtP le_total.
-Definition leP := TotalLattice.leP le_total.
-Definition ltP := TotalLattice.ltP le_total.
+Lemma le_nmono_in :
+  {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}}.
+Proof.
+move=> mf x y Dx Dy; case: ltgtP;
+  first (by move=> ->; apply/lexx); move/mf => fxy.
+- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT.
+- by apply/ltW/fxy.
+Qed.
 
+End TotalMonotonyTheory.
 End TotalTheory.
-End TotalTheory.
-
 
 Module Import BLatticeTheory.
 Section BLatticeTheory.
@@ -2149,8 +2335,8 @@ Implicit Types (x y z : L).
 Local Notation "0" := bottom.
 
 (* Distributive lattice theory with 0 & 1*)
-Lemma le0x x : 0 <= x. Proof. by case: L x => [?[?[]]]. Qed.
-Hint Resolve le0x.
+Lemma le0x x : 0 <= x. Proof. by case: L x => [?[? ?[]]]. Qed.
+Hint Resolve le0x : core.
 
 Lemma lex0 x : (x <= 0) = (x == 0).
 Proof. by rewrite le_eqVlt (le_gtF (le0x _)) orbF. Qed.
@@ -2183,7 +2369,7 @@ Proof. by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed.
 
 Lemma lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y).
 Proof.
-move=> xz0; apply/idP/idP=> xy; last by rewrite lexU ?xy.
+move=> xz0; apply/idP/idP=> xy; last by rewrite lexU2 ?xy.
 by apply: (@leU2l_le x z); rewrite ?joinxx.
 Qed.
 
@@ -2193,7 +2379,7 @@ Proof. by move=> xz0; rewrite joinC; rewrite lexUl. Qed.
 Lemma leU2E x y z t : x `&` t = 0 -> y `&` z = 0 ->
   (x `|` y <= z `|` t) = (x <= z) && (y <= t).
 Proof.
-move=> dxt dyz; apply/idP/andP; last by case=> ??; exact: leU2.
+move=> dxt dyz; apply/idP/andP; last by case=> ? ?; exact: leU2.
 by move=> lexyzt; rewrite (leU2l_le _ lexyzt) // (leU2r_le _ lexyzt).
 Qed.
 
@@ -2203,7 +2389,7 @@ apply/idP/idP; last by move=> /andP [/eqP-> /eqP->]; rewrite joinx0.
 by move=> /eqP xUy0; rewrite -!lex0 -!xUy0 ?leUl ?leUr.
 Qed.
 
-CoInductive eq0_xor_gt0 x : bool -> bool -> Set :=
+Variant eq0_xor_gt0 x : bool -> bool -> Set :=
     Eq0NotPOs : x = 0 -> eq0_xor_gt0 x true false
   | POsNotEq0 : 0 < x -> eq0_xor_gt0 x false true.
 
@@ -2213,15 +2399,15 @@ Proof. by rewrite lt0x; have [] := altP eqP; constructor; rewrite ?lt0x. Qed.
 Canonical join_monoid := Monoid.Law (@joinA _ _) join0x joinx0.
 Canonical join_comoid := Monoid.ComLaw (@joinC _ _).
 
-Lemma join_sup (I : finType) (j : I) (P : pred I) (F : I -> L) :
+Lemma join_sup (I : finType) (j : I) (P : {pred I}) (F : I -> L) :
    P j -> F j <= \join_(i | P i) F i.
-Proof. by move=> Pj; rewrite (bigD1 j) //= lexU ?lexx. Qed.
+Proof. by move=> Pj; rewrite (bigD1 j) //= lexU2 ?lexx. Qed.
 
-Lemma join_min (I : finType) (j : I) (l : L) (P : pred I) (F : I -> L) :
+Lemma join_min (I : finType) (j : I) (l : L) (P : {pred I}) (F : I -> L) :
    P j -> l <= F j -> l <= \join_(i | P i) F i.
 Proof. by move=> Pj /le_trans -> //; rewrite join_sup. Qed.
 
-Lemma joinsP (I : finType) (u : L) (P : pred I) (F : I -> L) :
+Lemma joinsP (I : finType) (u : L) (P : {pred I}) (F : I -> L) :
    reflect (forall i : I, P i -> F i <= u) (\join_(i | P i) F i <= u).
 Proof.
 have -> : \join_(i | P i) F i <= u = (\big[andb/true]_(i | P i) (F i <= u)).
@@ -2238,7 +2424,7 @@ move=> AsubB; rewrite -(setID B A).
 rewrite [X in _ <= X](eq_bigl [predU B :&: A & B :\: A]); last first.
   by move=> i; rewrite !inE.
 rewrite bigU //=; last by rewrite -setI_eq0 setDE setIACA setICr setI0.
-by rewrite lexU // (setIidPr _) // lexx.
+by rewrite lexU2 // (setIidPr _) // lexx.
 Qed.
 
 Lemma joins_setU (I : finType) (A B : {set I}) (F : I -> L) :
@@ -2246,7 +2432,7 @@ Lemma joins_setU (I : finType) (A B : {set I}) (F : I -> L) :
 Proof.
 apply/eqP; rewrite eq_le leUx !le_joins ?subsetUl ?subsetUr ?andbT //.
 apply/joinsP => i; rewrite inE; move=> /orP.
-by case=> ?; rewrite lexU //; [rewrite join_sup|rewrite orbC join_sup].
+by case=> ?; rewrite lexU2 //; [rewrite join_sup|rewrite orbC join_sup].
 Qed.
 
 Lemma join_seq (I : finType) (r : seq I) (F : I -> L) :
@@ -2256,11 +2442,11 @@ rewrite [RHS](eq_bigl (mem [set i | i \in r])); last by move=> i; rewrite !inE.
 elim: r => [|i r ihr]; first by rewrite big_nil big1 // => i; rewrite ?inE.
 rewrite big_cons {}ihr; apply/eqP; rewrite eq_le set_cons.
 rewrite leUx join_sup ?inE ?eqxx // le_joins //= ?subsetUr //.
-apply/joinsP => j; rewrite !inE => /predU1P [->|jr]; rewrite ?lexU ?lexx //.
+apply/joinsP => j; rewrite !inE => /predU1P [->|jr]; rewrite ?lexU2 ?lexx //.
 by rewrite join_sup ?orbT ?inE.
 Qed.
 
-Lemma joins_disjoint (I : finType) (d : L) (P : pred I) (F : I -> L) :
+Lemma joins_disjoint (I : finType) (d : L) (P : {pred I}) (F : I -> L) :
    (forall i : I, P i -> d `&` F i = 0) -> d `&` \join_(i | P i) F i = 0.
 Proof.
 move=> d_Fi_disj; have : \big[andb/true]_(i | P i) (d `&` F i == 0).
@@ -2274,84 +2460,84 @@ Qed.
 End BLatticeTheory.
 End BLatticeTheory.
 
-Module Import ReverseTBLattice.
-Section ReverseTBLattice.
+Module Import ConverseTBLattice.
+Section ConverseTBLattice.
 Context {disp : unit}.
 Local Notation tblatticeType := (tblatticeType disp).
 Context {L : tblatticeType}.
 
-Lemma lex1 (x : L) : x <= top. Proof. by case: L x => [?[?[]]]. Qed.
+Lemma lex1 (x : L) : x <= top. Proof. by case: L x => [?[? ?[]]]. Qed.
 
-Definition reverse_blatticeMixin :=
-  @BLatticeMixin _ [latticeType of L^r] top lex1.
-Canonical reverse_blatticeType := BLatticeType L^r reverse_blatticeMixin.
+Definition converse_blatticeMixin :=
+  @BLatticeMixin _ [latticeType of L^c] top lex1.
+Canonical converse_blatticeType := BLatticeType L^c converse_blatticeMixin.
 
-Definition reverse_tblatticeMixin :=
-   @TBLatticeMixin _ [latticeType of L^r] (bottom : L) (@le0x _ L).
-Canonical reverse_tblatticeType := TBLatticeType L^r reverse_tblatticeMixin.
+Definition converse_tblatticeMixin :=
+   @TBLatticeMixin _ [latticeType of L^c] (bottom : L) (@le0x _ L).
+Canonical converse_tblatticeType := TBLatticeType L^c converse_tblatticeMixin.
 
-End ReverseTBLattice.
-End ReverseTBLattice.
+End ConverseTBLattice.
+End ConverseTBLattice.
 
-Module Import ReverseTBLatticeSyntax.
-Section ReverseTBLatticeSyntax.
+Module Import ConverseTBLatticeSyntax.
+Section ConverseTBLatticeSyntax.
 Local Notation "0" := bottom.
 Local Notation "1" := top.
-Local Notation join := (@join (reverse_display _) _).
-Local Notation meet := (@meet (reverse_display _) _).
+Local Notation join := (@join (converse_display _) _).
+Local Notation meet := (@meet (converse_display _) _).
 
-Notation "\join^r_ ( i <- r | P ) F" :=
+Notation "\join^c_ ( i <- r | P ) F" :=
   (\big[join/0]_(i <- r | P%B) F%O) : order_scope.
-Notation "\join^r_ ( i <- r ) F" :=
+Notation "\join^c_ ( i <- r ) F" :=
   (\big[join/0]_(i <- r) F%O) : order_scope.
-Notation "\join^r_ ( i | P ) F" :=
+Notation "\join^c_ ( i | P ) F" :=
   (\big[join/0]_(i | P%B) F%O) : order_scope.
-Notation "\join^r_ i F" :=
+Notation "\join^c_ i F" :=
   (\big[join/0]_i F%O) : order_scope.
-Notation "\join^r_ ( i : I | P ) F" :=
+Notation "\join^c_ ( i : I | P ) F" :=
   (\big[join/0]_(i : I | P%B) F%O) (only parsing) : order_scope.
-Notation "\join^r_ ( i : I ) F" :=
+Notation "\join^c_ ( i : I ) F" :=
   (\big[join/0]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\join^r_ ( m <= i < n | P ) F" :=
+Notation "\join^c_ ( m <= i < n | P ) F" :=
  (\big[join/0]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\join^r_ ( m <= i < n ) F" :=
+Notation "\join^c_ ( m <= i < n ) F" :=
  (\big[join/0]_(m <= i < n) F%O) : order_scope.
-Notation "\join^r_ ( i < n | P ) F" :=
+Notation "\join^c_ ( i < n | P ) F" :=
  (\big[join/0]_(i < n | P%B) F%O) : order_scope.
-Notation "\join^r_ ( i < n ) F" :=
+Notation "\join^c_ ( i < n ) F" :=
  (\big[join/0]_(i < n) F%O) : order_scope.
-Notation "\join^r_ ( i 'in' A | P ) F" :=
+Notation "\join^c_ ( i 'in' A | P ) F" :=
  (\big[join/0]_(i in A | P%B) F%O) : order_scope.
-Notation "\join^r_ ( i 'in' A ) F" :=
+Notation "\join^c_ ( i 'in' A ) F" :=
  (\big[join/0]_(i in A) F%O) : order_scope.
 
-Notation "\meet^r_ ( i <- r | P ) F" :=
+Notation "\meet^c_ ( i <- r | P ) F" :=
   (\big[meet/1]_(i <- r | P%B) F%O) : order_scope.
-Notation "\meet^r_ ( i <- r ) F" :=
+Notation "\meet^c_ ( i <- r ) F" :=
   (\big[meet/1]_(i <- r) F%O) : order_scope.
-Notation "\meet^r_ ( i | P ) F" :=
+Notation "\meet^c_ ( i | P ) F" :=
   (\big[meet/1]_(i | P%B) F%O) : order_scope.
-Notation "\meet^r_ i F" :=
+Notation "\meet^c_ i F" :=
   (\big[meet/1]_i F%O) : order_scope.
-Notation "\meet^r_ ( i : I | P ) F" :=
+Notation "\meet^c_ ( i : I | P ) F" :=
   (\big[meet/1]_(i : I | P%B) F%O) (only parsing) : order_scope.
-Notation "\meet^r_ ( i : I ) F" :=
+Notation "\meet^c_ ( i : I ) F" :=
   (\big[meet/1]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\meet^r_ ( m <= i < n | P ) F" :=
+Notation "\meet^c_ ( m <= i < n | P ) F" :=
  (\big[meet/1]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\meet^r_ ( m <= i < n ) F" :=
+Notation "\meet^c_ ( m <= i < n ) F" :=
  (\big[meet/1]_(m <= i < n) F%O) : order_scope.
-Notation "\meet^r_ ( i < n | P ) F" :=
+Notation "\meet^c_ ( i < n | P ) F" :=
  (\big[meet/1]_(i < n | P%B) F%O) : order_scope.
-Notation "\meet^r_ ( i < n ) F" :=
+Notation "\meet^c_ ( i < n ) F" :=
  (\big[meet/1]_(i < n) F%O) : order_scope.
-Notation "\meet^r_ ( i 'in' A | P ) F" :=
+Notation "\meet^c_ ( i 'in' A | P ) F" :=
  (\big[meet/1]_(i in A | P%B) F%O) : order_scope.
-Notation "\meet^r_ ( i 'in' A ) F" :=
+Notation "\meet^c_ ( i 'in' A ) F" :=
  (\big[meet/1]_(i in A) F%O) : order_scope.
 
-End ReverseTBLatticeSyntax.
-End ReverseTBLatticeSyntax.
+End ConverseTBLatticeSyntax.
+End ConverseTBLatticeSyntax.
 
 Module Import TBLatticeTheory.
 Section TBLatticeTheory.
@@ -2362,43 +2548,43 @@ Implicit Types (x y : L).
 
 Local Notation "1" := top.
 
-Hint Resolve le0x lex1.
+Hint Resolve le0x lex1 : core.
 
 Lemma meetx1 : right_id 1 (@meet _ L).
-Proof. exact: (@joinx0 _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@joinx0 _ [tblatticeType of L^c]). Qed.
 
 Lemma meet1x : left_id 1 (@meet _ L).
-Proof. exact: (@join0x _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@join0x _ [tblatticeType of L^c]). Qed.
 
 Lemma joinx1 : right_zero 1 (@join _ L).
-Proof. exact: (@meetx0 _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@meetx0 _ [tblatticeType of L^c]). Qed.
 
 Lemma join1x : left_zero 1 (@join _ L).
-Proof. exact: (@meet0x _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@meet0x _ [tblatticeType of L^c]). Qed.
 
 Lemma le1x x : (1 <= x) = (x == 1).
-Proof. exact: (@lex0 _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@lex0 _ [tblatticeType of L^c]). Qed.
 
 Lemma leI2l_le y t x z : y `|` z = 1 -> x `&` y <= z `&` t -> x <= z.
-Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^r]). Qed.
+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^r]). Qed.
+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^r]). Qed.
+Proof. rewrite joinC; exact: (@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^r]). Qed.
+Proof. rewrite joinC; exact: (@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).
 Proof.
-by move=> ? ?; apply: (@leU2E _ [tblatticeType of L^r]); rewrite meetC.
+by move=> ? ?; apply: (@leU2E _ [tblatticeType of L^c]); rewrite meetC.
 Qed.
 
 Lemma meet_eq1 x y : (x `&` y == 1) = (x == 1) && (y == 1).
-Proof. exact: (@join_eq0 _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@join_eq0 _ [tblatticeType of L^c]). Qed.
 
 Canonical meet_monoid := Monoid.Law (@meetA _ _) meet1x meetx1.
 Canonical meet_comoid := Monoid.ComLaw (@meetC _ _).
@@ -2408,33 +2594,33 @@ Canonical join_muloid := Monoid.MulLaw join1x joinx1.
 Canonical join_addoid := Monoid.AddLaw (@meetUl _ L) (@meetUr _ _).
 Canonical meet_addoid := Monoid.AddLaw (@joinIl _ L) (@joinIr _ _).
 
-Lemma meets_inf (I : finType) (j : I) (P : pred I) (F : I -> L) :
+Lemma meets_inf (I : finType) (j : I) (P : {pred I}) (F : I -> L) :
    P j -> \meet_(i | P i) F i <= F j.
-Proof. exact: (@join_sup _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@join_sup _ [tblatticeType of L^c]). Qed.
 
-Lemma meets_max (I : finType) (j : I) (u : L) (P : pred I) (F : I -> L) :
+Lemma meets_max (I : finType) (j : I) (u : L) (P : {pred I}) (F : I -> L) :
    P j -> F j <= u -> \meet_(i | P i) F i <= u.
-Proof. exact: (@join_min _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@join_min _ [tblatticeType of L^c]). Qed.
 
-Lemma meetsP (I : finType) (l : L) (P : pred I) (F : I -> L) :
+Lemma meetsP (I : finType) (l : L) (P : {pred I}) (F : I -> L) :
    reflect (forall i : I, P i -> l <= F i) (l <= \meet_(i | P i) F i).
-Proof. exact: (@joinsP _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@joinsP _ [tblatticeType of L^c]). Qed.
 
 Lemma le_meets (I : finType) (A B : {set I}) (F : I -> L) :
    A \subset B -> \meet_(i in B) F i <= \meet_(i in A) F i.
-Proof. exact: (@le_joins _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@le_joins _ [tblatticeType of L^c]). Qed.
 
 Lemma meets_setU (I : finType) (A B : {set I}) (F : I -> L) :
    \meet_(i in (A :|: B)) F i = \meet_(i in A) F i `&` \meet_(i in B) F i.
-Proof. exact: (@joins_setU _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@joins_setU _ [tblatticeType of L^c]). Qed.
 
 Lemma meet_seq (I : finType) (r : seq I) (F : I -> L) :
    \meet_(i <- r) F i = \meet_(i in r) F i.
-Proof. exact: (@join_seq _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@join_seq _ [tblatticeType of L^c]). Qed.
 
-Lemma meets_total (I : finType) (d : L) (P : pred I) (F : I -> L) :
+Lemma meets_total (I : finType) (d : L) (P : {pred I}) (F : I -> L) :
    (forall i : I, P i -> d `|` F i = 1) -> d `|` \meet_(i | P i) F i = 1.
-Proof. exact: (@joins_disjoint _ [tblatticeType of L^r]). Qed.
+Proof. exact: (@joins_disjoint _ [tblatticeType of L^c]). Qed.
 
 End TBLatticeTheory.
 End TBLatticeTheory.
@@ -2448,7 +2634,7 @@ Implicit Types (x y z : L).
 Local Notation "0" := bottom.
 
 Lemma subKI x y : y `&` (x `\` y) = 0.
-Proof. by case: L x y => ? [? []]. Qed.
+Proof. by case: L x y => ? [? ?[]]. Qed.
 
 Lemma subIK x y : (x `\` y) `&` y = 0.
 Proof. by rewrite meetC subKI. Qed.
@@ -2460,7 +2646,7 @@ Lemma meetBI z x y : (x `\` y) `&` (z `&` y) = 0.
 Proof. by rewrite meetC meetIB. Qed.
 
 Lemma joinIB y x : (x `&` y) `|` (x `\` y) = x.
-Proof. by case: L x y => ? [? []]. Qed.
+Proof. by case: L x y => ? [? ?[]]. Qed.
 
 Lemma joinBI y x : (x `\` y) `|` (x `&` y) = x.
 Proof. by rewrite joinC joinIB. Qed.
@@ -2472,8 +2658,8 @@ Lemma joinBIC y x : (x `\` y) `|` (y `&` x) = x.
 Proof. by rewrite meetC joinBI. Qed.
 
 Lemma leBx x y : x `\` y <= x.
-Proof. by rewrite -{2}[x](joinIB y) lexU // lexx orbT. Qed.
-Hint Resolve leBx.
+Proof. by rewrite -{2}[x](joinIB y) lexU2 // lexx orbT. Qed.
+Hint Resolve leBx : core.
 
 Lemma subxx x : x `\` x = 0.
 Proof. by have := subKI x x; rewrite (meet_idPr _). Qed.
@@ -2522,7 +2708,7 @@ Proof. by rewrite ![_ `|` x]joinC ![_ `&` x]meetC joinxB. Qed.
 
 Lemma leBr z x y : x <= y -> z `\` y <= z `\` x.
 Proof.
-by move=> lexy; rewrite leBLR joinxB (meet_idPr _) ?leBUK ?leUr ?lexU ?lexy.
+by move=> lexy; rewrite leBLR joinxB (meet_idPr _) ?leBUK ?leUr ?lexU2 ?lexy.
 Qed.
 
 Lemma leB2 x y z t : x <= z -> t <= y -> x `\` y <= z `\` t.
@@ -2546,7 +2732,7 @@ Proof. by rewrite eq_le leBLR leBRL andbCA andbA. Qed.
 Lemma subxU x y z : z `\` (x `|` y) = (z `\` x) `&` (z `\` y).
 Proof.
 apply/eqP; rewrite eq_le lexI !leBr ?leUl ?leUr //=.
-rewrite leBRL leIx ?leBx //= meetUr meetAC subIK -meetA subIK.
+rewrite leBRL leIx2 ?leBx //= meetUr meetAC subIK -meetA subIK.
 by rewrite meet0x meetx0 joinx0.
 Qed.
 
@@ -2628,7 +2814,7 @@ Local Notation "0" := bottom.
 Local Notation "1" := top.
 
 Lemma complE x : ~` x = 1 `\` x.
-Proof. by case: L x => [? [? ? []]]. Qed.
+Proof. by case: L x => [?[? ? ? ?[]]]. Qed.
 
 Lemma sub1x x : 1 `\` x = ~` x.
 Proof. by rewrite complE. Qed.
@@ -2688,11 +2874,11 @@ Proof. by rewrite !complE !leBLR joinC. Qed.
 Lemma lexC x y : (x <= ~` y) = (y <= ~` x).
 Proof. by rewrite !complE !leBRL !lex1 meetC. Qed.
 
-Lemma compl_joins (J : Type) (r : seq J) (P : pred J) (F : J -> L) :
+Lemma compl_joins (J : Type) (r : seq J) (P : {pred J}) (F : J -> L) :
    ~` (\join_(j <- r | P j) F j) = \meet_(j <- r | P j) ~` F j.
 Proof. by elim/big_rec2: _=> [|i x y ? <-]; rewrite ?compl0 ?complU. Qed.
 
-Lemma compl_meets (J : Type) (r : seq J) (P : pred J) (F : J -> L) :
+Lemma compl_meets (J : Type) (r : seq J) (P : {pred J}) (F : J -> L) :
    ~` (\meet_(j <- r | P j) F j) = \join_(j <- r | P j) ~` F j.
 Proof. by elim/big_rec2: _=> [|i x y ? <-]; rewrite ?compl1 ?complI. Qed.
 
@@ -2700,95 +2886,741 @@ End CTBLatticeTheory.
 End CTBLatticeTheory.
 
 (*************)
+(* FACTORIES *)
+(*************)
+
+Module TotalLatticeMixin.
+Section TotalLatticeMixin.
+Import POrderDef.
+Variable (disp : unit) (T : porderType disp).
+Definition of_ := total (<=%O : rel T).
+Variable (m : of_).
+Implicit Types (x y z : T).
+
+Let comparableT x y : x >=< y := m x y.
+
+Fact ltgtP x y :
+  comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y).
+Proof. exact: comparable_ltgtP. Qed.
+
+Fact leP x y : le_xor_gt x y (x <= y) (y < x).
+Proof. exact: comparable_leP. Qed.
+
+Fact ltP x y : lt_xor_ge x y (y <= x) (x < y).
+Proof. exact: comparable_ltP. Qed.
+
+Definition meet x y := if x <= y then x else y.
+Definition join x y := if y <= x then x else y.
+
+Fact meetC : commutative meet.
+Proof. by move=> x y; rewrite /meet; have [] := ltgtP. Qed.
+
+Fact joinC : commutative join.
+Proof. by move=> x y; rewrite /join; have [] := ltgtP. Qed.
+
+Fact meetA : associative meet.
+Proof.
+move=> x y z; rewrite /meet; case: (leP y z) => yz; case: (leP x y) => xy //=.
+- by rewrite (le_trans xy).
+- by rewrite yz.
+by rewrite !lt_geF // (lt_trans yz).
+Qed.
+
+Fact joinA : associative join.
+Proof.
+move=> x y z; rewrite /join; case: (leP z y) => yz; case: (leP y x) => xy //=.
+- by rewrite (le_trans yz).
+- by rewrite yz.
+by rewrite !lt_geF // (lt_trans xy).
+Qed.
+
+Fact joinKI y x : meet x (join x y) = x.
+Proof. by rewrite /meet /join; case: (leP y x) => yx; rewrite ?lexx ?ltW. Qed.
+
+Fact meetKU y x : join x (meet x y) = x.
+Proof. by rewrite /meet /join; case: (leP x y) => yx; rewrite ?lexx ?ltW. Qed.
+
+Fact leEmeet x y : (x <= y) = (meet x y == x).
+Proof. by rewrite /meet; case: leP => ?; rewrite ?eqxx ?lt_eqF. Qed.
+
+Fact meetUl : left_distributive meet join.
+Proof.
+move=> x y z; rewrite /meet /join.
+case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last.
+- by rewrite yz [x <= z](le_trans _ yz) ?[x <= y]ltW // lt_geF.
+- by rewrite lt_geF ?lexx // (lt_le_trans yz).
+- by rewrite lt_geF //; have [->|/lt_geF->|] := (ltgtP x z); rewrite ?lexx.
+- by have [] := (leP x z); rewrite ?xy ?yz.
+Qed.
+
+Definition latticeMixin :=
+  LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+
+End TotalLatticeMixin.
+
+Module Exports.
+Notation totalLatticeMixin := of_.
+Coercion latticeMixin : totalLatticeMixin >-> Order.Lattice.mixin_of.
+End Exports.
+
+End TotalLatticeMixin.
+Import TotalLatticeMixin.Exports.
+
+Module LePOrderMixin.
+Section LePOrderMixin.
+Variable (T : eqType).
+
+Record of_ := Build {
+  le : rel T;
+  lt : rel T;
+  le_refl  : reflexive le;
+  le_anti  : antisymmetric le;
+  le_trans : transitive le;
+  lt_def   : forall x y, lt x y = (y != x) && le x y;
+}.
+
+Definition porderMixin (m : of_) : porderMixin T :=
+   POrderMixin (@lt_def m) (@le_refl m) (@le_anti m) (@le_trans m).
+
+End LePOrderMixin.
+
+Module Exports.
+Notation lePOrderMixin := of_.
+Notation LePOrderMixin := Build.
+Coercion porderMixin : lePOrderMixin >-> POrder.mixin_of.
+End Exports.
+
+End LePOrderMixin.
+Import LePOrderMixin.Exports.
+
+Module LtPOrderMixin.
+Section LtPOrderMixin.
+Variable (T : eqType).
+
+Record of_ := Build {
+  le : rel T;
+  lt : rel T;
+  lt_irr   : irreflexive lt;
+  lt_trans : transitive lt;
+  le_def   : forall x y, le x y = (x == y) || lt x y;
+}.
+
+Variable (m : of_).
+
+Fact lt_asym x y : (lt m x y && lt m y x) = false.
+Proof.
+by apply/negP => /andP [] xy /(lt_trans xy); apply/negP; rewrite (lt_irr m x).
+Qed.
+
+Fact lt_def x y : lt m x y = (y != x) && le m x y.
+Proof. by rewrite le_def eq_sym; case: eqP => //= <-; rewrite lt_irr. Qed.
+
+Fact le_refl : reflexive (le m).
+Proof. by move=> ?; rewrite le_def eqxx. Qed.
+
+Fact le_anti : antisymmetric (le m).
+Proof.
+by move=> ? ?; rewrite !le_def eq_sym -orb_andr lt_asym orbF => /eqP.
+Qed.
+
+Fact le_trans : transitive (le m).
+Proof.
+by move=> y x z; rewrite !le_def => /predU1P [-> //|ltxy] /predU1P [<-|ltyz];
+  rewrite ?ltxy ?(lt_trans ltxy ltyz) // ?orbT.
+Qed.
+
+Definition porderMixin : porderMixin T :=
+   @POrderMixin _ (le m) (lt m) lt_def le_refl le_anti le_trans.
+
+End LtPOrderMixin.
+
+Module Exports.
+Notation ltPOrderMixin := of_.
+Notation LtPOrderMixin := Build.
+Coercion porderMixin : ltPOrderMixin >-> POrder.mixin_of.
+End Exports.
+
+End LtPOrderMixin.
+Import LtPOrderMixin.Exports.
+
+Module MeetJoinMixin.
+Section MeetJoinMixin.
+
+Variable (disp : unit) (T : choiceType).
+
+Record of_ (disp : unit) (T : choiceType) := Build {
+  le : rel T;
+  lt : rel T;
+  meet : T -> T -> T;
+  join : T -> T -> T;
+  meetC : commutative meet;
+  joinC : commutative join;
+  meetA : associative meet;
+  joinA : associative join;
+  joinKI : forall y x : T, meet x (join x y) = x;
+  meetKU : forall y x : T, join x (meet x y) = x;
+  meetUl : left_distributive meet join;
+  meetxx : idempotent meet;
+  le_def : forall x y : T, le x y = (meet x y == x);
+  lt_def : forall x y : T, lt x y = (y != x) && le x y;
+}.
+
+
+Variable (m : of_ disp T).
+
+Fact le_refl : reflexive (le m).
+Proof. by move=> x; rewrite le_def meetxx. Qed.
+
+Fact le_anti : antisymmetric (le m).
+Proof. by move=> x y; rewrite !le_def meetC => /andP [] /eqP {2}<- /eqP ->. Qed.
+
+Fact le_trans : transitive (le m).
+Proof.
+move=> y x z; rewrite !le_def => /eqP lexy /eqP leyz; apply/eqP.
+by rewrite -[in LHS]lexy -meetA leyz lexy.
+Qed.
+
+Definition porderMixin : lePOrderMixin T :=
+  LePOrderMixin le_refl le_anti le_trans (lt_def m).
+
+Definition latticeMixin : latticeMixin (POrderType disp T porderMixin) :=
+  @LatticeMixin disp (POrderType disp T porderMixin) (meet m) (join m)
+                (meetC m) (joinC m) (meetA m) (joinA m)
+                (joinKI m) (meetKU m) (le_def m) (meetUl m).
+
+End MeetJoinMixin.
+
+Module Exports.
+Notation meetJoinMixin := of_.
+Notation MeetJoinMixin := Build.
+Coercion porderMixin : meetJoinMixin >-> lePOrderMixin.
+Coercion latticeMixin : meetJoinMixin >-> Lattice.mixin_of.
+End Exports.
+
+End MeetJoinMixin.
+Import MeetJoinMixin.Exports.
+
+Module LeOrderMixin.
+Section LeOrderMixin.
+
+Record of_ (disp : unit) (T : choiceType) := Build {
+  le : rel T;
+  lt : rel T;
+  meet : T -> T -> T;
+  join : T -> T -> T;
+  le_anti : antisymmetric le;
+  le_trans : transitive le;
+  le_total : total le;
+  lt_def : forall x y, lt x y = (y != x) && le x y;
+  meet_def : forall x y, meet x y = if le x y then x else y;
+  join_def : forall x y, join x y = if le y x then x else y;
+}.
+
+Variable (disp : unit) (T : choiceType) (m : of_ disp T).
+
+Fact le_refl : reflexive (le m).
+Proof. by move=> x; case: (le m x x) (le_total m x x). Qed.
+
+Definition T_porderType : porderType disp :=
+  POrderType
+    disp T
+    (LePOrderMixin le_refl (@le_anti _ _ m) (@le_trans _ _ m) (lt_def m)).
+Definition T_latticeType : latticeType disp :=
+  LatticeType T_porderType (le_total m : totalLatticeMixin T_porderType).
+
+Implicit Types (x y z : T_latticeType).
+
+Fact meetE x y : meet m x y = x `&` y. Proof. by rewrite meet_def. Qed.
+Fact joinE x y : join m x y = x `|` y. Proof. by rewrite join_def. Qed.
+Fact meetC : commutative (meet m).
+Proof. by move=> *; rewrite !meetE meetC. Qed.
+Fact joinC : commutative (join m).
+Proof. by move=> *; rewrite !joinE joinC. Qed.
+Fact meetA : associative (meet m).
+Proof. by move=> *; rewrite !meetE meetA. Qed.
+Fact joinA : associative (join m).
+Proof. by move=> *; rewrite !joinE joinA. Qed.
+Fact joinKI y x : meet m x (join m x y) = x.
+Proof. by rewrite meetE joinE joinKI. Qed.
+Fact meetKU y x : join m x (meet m x y) = x.
+Proof. by rewrite meetE joinE meetKU. Qed.
+Fact meetUl : left_distributive (meet m) (join m).
+Proof. by move=> *; rewrite !meetE !joinE meetUl. Qed.
+Fact meetxx : idempotent (meet m).
+Proof. by move=> *; rewrite meetE meetxx. Qed.
+Fact le_def x y : x <= y = (meet m x y == x).
+Proof. by rewrite meetE (eq_meetl x y). Qed.
+
+Definition latticeMixin : meetJoinMixin disp T :=
+  @MeetJoinMixin
+    _ _ (le m) (lt m) (meet m) (join m)
+    meetC joinC meetA joinA joinKI meetKU meetUl meetxx le_def (lt_def m).
+
+Definition totalMixin :
+  Total.mixin_of (LatticeType (POrderType disp T latticeMixin) latticeMixin)
+  := le_total m.
+
+End LeOrderMixin.
+
+Module Exports.
+Notation leOrderMixin := of_.
+Notation LeOrderMixin := Build.
+Coercion latticeMixin : leOrderMixin >-> meetJoinMixin.
+Coercion totalMixin : leOrderMixin >-> Total.mixin_of.
+End Exports.
+
+End LeOrderMixin.
+Import LeOrderMixin.Exports.
+
+Module LtOrderMixin.
+
+Record of_ (disp : unit) (T : choiceType) := Build {
+  le : rel T;
+  lt : rel T;
+  meet : T -> T -> T;
+  join : T -> T -> T;
+  lt_irr   : irreflexive lt;
+  lt_trans : transitive lt;
+  lt_total : forall x y, x != y -> lt x y || lt y x;
+  le_def   : forall x y, le x y = (x == y) || lt x y;
+  meet_def : forall x y, meet x y = if lt x y then x else y;
+  join_def : forall x y, join x y = if lt y x then x else y;
+}.
+
+Section LtOrderMixin.
+
+Variable (disp : unit) (T : choiceType) (m : of_ disp T).
+
+Fact le_total : total (le m).
+Proof.
+by move=> x y; rewrite !le_def (eq_sym y); case: (altP eqP); [|apply: lt_total].
+Qed.
+
+Definition T_porderType : porderType disp :=
+  POrderType disp T (LtPOrderMixin (lt_irr m) (@lt_trans _ _ m) (le_def m)).
+Definition T_latticeType : latticeType disp :=
+  LatticeType T_porderType (le_total : totalLatticeMixin T_porderType).
+
+Implicit Types (x y z : T_latticeType).
+
+Fact leP x y :
+  le_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+Proof. by apply/lcomparable_leP/le_total. Qed.
+Fact meetE x y : meet m x y = x `&` y.
+Proof. by rewrite meet_def (_ : lt m x y = (x < y)) //; case: (leP y). Qed.
+Fact joinE x y : join m x y = x `|` y.
+Proof. by rewrite join_def (_ : lt m y x = (y < x)) //; case: leP. Qed.
+Fact meetC : commutative (meet m).
+Proof. by move=> *; rewrite !meetE meetC. Qed.
+Fact joinC : commutative (join m).
+Proof. by move=> *; rewrite !joinE joinC. Qed.
+Fact meetA : associative (meet m).
+Proof. by move=> *; rewrite !meetE meetA. Qed.
+Fact joinA : associative (join m).
+Proof. by move=> *; rewrite !joinE joinA. Qed.
+Fact joinKI y x : meet m x (join m x y) = x.
+Proof. by rewrite meetE joinE joinKI. Qed.
+Fact meetKU y x : join m x (meet m x y) = x.
+Proof. by rewrite meetE joinE meetKU. Qed.
+Fact meetUl : left_distributive (meet m) (join m).
+Proof. by move=> *; rewrite !meetE !joinE meetUl. Qed.
+Fact meetxx : idempotent (meet m).
+Proof. by move=> *; rewrite meetE meetxx. Qed.
+Fact le_def' x y : x <= y = (meet m x y == x).
+Proof. by rewrite meetE (eq_meetl x y). Qed.
+
+Definition latticeMixin : meetJoinMixin disp T :=
+  @MeetJoinMixin
+    _ _ (le m) (lt m) (meet m) (join m)
+    meetC joinC meetA joinA joinKI meetKU meetUl meetxx
+    le_def' (@lt_def _ T_latticeType).
+
+Definition totalMixin :
+  Total.mixin_of (LatticeType (POrderType disp T latticeMixin) latticeMixin)
+  := le_total.
+
+End LtOrderMixin.
+
+Module Exports.
+Notation ltOrderMixin := of_.
+Notation LtOrderMixin := Build.
+Coercion latticeMixin : ltOrderMixin >-> meetJoinMixin.
+Coercion totalMixin : ltOrderMixin >-> Total.mixin_of.
+End Exports.
+
+End LtOrderMixin.
+Import LtOrderMixin.Exports.
+
+(*************)
 (* INSTANCES *)
 (*************)
 
-Module Import NatOrder.
+Module NatOrder.
 Section NatOrder.
 
-Fact nat_display : unit. Proof. exact: tt. Qed.
-Program Definition natPOrderMixin := @POrderMixin _ leq ltn _ leqnn anti_leq leq_trans.
-Next Obligation. by rewrite ltn_neqAle. Qed.
-Canonical natPOrderType  := POrderType nat_display nat natPOrderMixin.
+Lemma minnE x y : minn x y = if (x <= y)%N then x else y.
+Proof. by case: leqP => [/minn_idPl|/ltnW /minn_idPr]. Qed.
 
-Lemma leEnat (n m : nat): (n <= m) = (n <= m)%N.
+Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y.
+Proof. by case: leqP => [/maxn_idPl|/ltnW/maxn_idPr]. Qed.
+
+Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
+Proof. by rewrite ltn_neqAle eq_sym. Qed.
+
+Definition orderMixin :=
+  LeOrderMixin total_display anti_leq leq_trans leq_total ltn_def minnE maxnE.
+
+Canonical porderType := POrderType total_display nat orderMixin.
+Canonical latticeType := LatticeType nat orderMixin.
+Canonical orderType := OrderType nat orderMixin.
+Canonical blatticeType := BLatticeType nat (BLatticeMixin leq0n).
+
+Lemma leEnat: le = leq.
 Proof. by []. Qed.
 
 Lemma ltEnat (n m : nat): (n < m) = (n < m)%N.
 Proof. by []. Qed.
 
-Definition natLatticeMixin := TotalLattice.Mixin leq_total.
-Canonical natLatticeType := LatticeType nat natLatticeMixin.
-Canonical natOrderType := OrderType nat leq_total.
-
-Definition natBLatticeMixin := BLatticeMixin leq0n.
-Canonical natBLatticeType := BLatticeType nat natBLatticeMixin.
+End NatOrder.
+Module Exports.
+Canonical porderType.
+Canonical latticeType.
+Canonical orderType.
+Canonical blatticeType.
+Definition leEnat := leEnat.
+Definition ltEnat := ltEnat.
+End Exports.
 End NatOrder.
 
-Notation "@max" := (@join nat_display).
-Notation max := (@join nat_display _).
-Notation "@min" := (@meet nat_display).
-Notation min := (@meet nat_display _).
+Module ProductOrder.
+Section ProductOrder.
+Context {disp1 disp2 disp3 : unit}.
 
-Notation "\max_ ( i <- r | P ) F" :=
-  (\big[@join nat_display _/0%O]_(i <- r | P%B) F%O) : order_scope.
-Notation "\max_ ( i <- r ) F" :=
-  (\big[@join nat_display _/0%O]_(i <- r) F%O) : order_scope.
-Notation "\max_ ( i | P ) F" :=
-  (\big[@join nat_display _/0%O]_(i | P%B) F%O) : order_scope.
-Notation "\max_ i F" :=
-  (\big[@join nat_display _/0%O]_i F%O) : order_scope.
-Notation "\max_ ( i : I | P ) F" :=
-  (\big[@join nat_display _/0%O]_(i : I | P%B) F%O) (only parsing) : order_scope.
-Notation "\max_ ( i : I ) F" :=
-  (\big[@join nat_display _/0%O]_(i : I) F%O) (only parsing) : order_scope.
-Notation "\max_ ( m <= i < n | P ) F" :=
- (\big[@join nat_display _/0%O]_(m <= i < n | P%B) F%O) : order_scope.
-Notation "\max_ ( m <= i < n ) F" :=
- (\big[@join nat_display _/0%O]_(m <= i < n) F%O) : order_scope.
-Notation "\max_ ( i < n | P ) F" :=
- (\big[@join nat_display _/0%O]_(i < n | P%B) F%O) : order_scope.
-Notation "\max_ ( i < n ) F" :=
- (\big[@join nat_display _/0%O]_(i < n) F%O) : order_scope.
-Notation "\max_ ( i 'in' A | P ) F" :=
- (\big[@join nat_display _/0%O]_(i in A | P%B) F%O) : order_scope.
-Notation "\max_ ( i 'in' A ) F" :=
- (\big[@join nat_display _/0%O]_(i in A) F%O) : order_scope.
+Section POrder.
+Variable (T : porderType disp1) (T' : porderType disp2).
 
-End NatOrder.
+Definition le (x y : T * T') := (x.1 <= y.1) && (x.2 <= y.2).
 
+Fact refl : reflexive le.
+Proof. by move=> ?; rewrite /le !lexx. Qed.
 
-Module SeqLexPOrder.
-Section SeqLexPOrder.
-Context {display : unit}.
-Local Notation porderType := (porderType display).
-Variable T : porderType.
+Fact anti : antisymmetric le.
+Proof.
+case=> [? ?] [? ?].
+by rewrite andbAC andbA andbAC -andbA => /= /andP [] /le_anti -> /le_anti ->.
+Qed.
+
+Fact trans : transitive le.
+Proof.
+rewrite /le => y x z /andP [] hxy ? /andP [] /(le_trans hxy) ->.
+by apply: le_trans.
+Qed.
+
+Definition porderMixin := LePOrderMixin refl anti trans (rrefl _).
+Canonical porderType := POrderType disp3 (T * T') porderMixin.
+
+End POrder.
+
+Section Lattice.
+Variable (T : latticeType disp1) (T' : latticeType disp2).
+Implicit Types (x y : T * T').
+
+Definition meet x y := (x.1 `&` y.1, x.2 `&` y.2).
+Definition join x y := (x.1 `|` y.1, x.2 `|` y.2).
+
+Fact meetC : commutative meet.
+Proof. by move=> ? ?; congr pair; rewrite meetC. Qed.
+
+Fact joinC : commutative join.
+Proof. by move=> ? ?; congr pair; rewrite joinC. Qed.
+
+Fact meetA : associative meet.
+Proof. by move=> ? ? ?; congr pair; rewrite meetA. Qed.
+
+Fact joinA : associative join.
+Proof. by move=> ? ? ?; congr pair; rewrite joinA. Qed.
+
+Fact joinKI y x : meet x (join x y) = x.
+Proof. by case: x => ? ?; congr pair; rewrite joinKI. Qed.
+
+Fact meetKU y x : join x (meet x y) = x.
+Proof. by case: x => ? ?; congr pair; rewrite meetKU. Qed.
+
+Fact leEmeet x y : (x <= y) = (meet x y == x).
+Proof. by rewrite /POrderDef.le /= /le /meet eqE /= -!leEmeet. Qed.
+
+Fact meetUl : left_distributive meet join.
+Proof. by move=> ? ? ?; congr pair; rewrite meetUl. Qed.
+
+Definition latticeMixin :=
+  Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+Canonical latticeType := LatticeType (T * T') latticeMixin.
+
+End Lattice.
+
+Section BLattice.
+Variable (T : blatticeType disp1) (T' : blatticeType disp2).
+
+Fact le0x (x : T * T') : (0, 0) <= x.
+Proof. by rewrite /POrderDef.le /= /le !le0x. Qed.
+
+Canonical blatticeType := BLatticeType (T * T') (BLattice.Mixin le0x).
+
+End BLattice.
+
+Section TBLattice.
+Variable (T : tblatticeType disp1) (T' : tblatticeType disp2).
+
+Fact lex1 (x : T * T') : x <= (top, top).
+Proof. by rewrite /POrderDef.le /= /le !lex1. Qed.
+
+Canonical tblatticeType := TBLatticeType (T * T') (TBLattice.Mixin lex1).
+
+End TBLattice.
+
+Section CBLattice.
+Variable (T : cblatticeType disp1) (T' : cblatticeType disp2).
+Implicit Types (x y : T * T').
+
+Definition sub x y := (x.1 `\` y.1, x.2 `\` y.2).
+
+Lemma subKI x y : y `&` (sub x y) = 0.
+Proof. by congr pair; rewrite subKI. Qed.
+
+Lemma joinIB x y : (x `&` y) `|` (sub x y) = x.
+Proof. by case: x => ? ?; congr pair; rewrite joinIB. Qed.
+
+Definition cblatticeMixin := CBLattice.Mixin subKI joinIB.
+Canonical cblatticeType := CBLatticeType (T * T') cblatticeMixin.
+
+End CBLattice.
+
+Section CTBLattice.
+Variable (T : ctblatticeType disp1) (T' : ctblatticeType disp2).
+Implicit Types (x y : T * T').
+
+Definition compl x := (~` x.1, ~` x.2).
+
+Lemma complE x : compl x = sub 1 x.
+Proof. by congr pair; rewrite complE. Qed.
+
+Definition ctblatticeMixin := CTBLattice.Mixin complE.
+Canonical ctblatticeType := CTBLatticeType (T * T') ctblatticeMixin.
+(* Let default_ctblatticeType := [default_ctblatticeType of T * T']. *)
+
+End CTBLattice.
+
+Canonical finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) :=
+  [finPOrderType of T * T'].
+
+Canonical finLatticeType
+          (T : finLatticeType disp1) (T' : finLatticeType disp2) :=
+  [finLatticeType of T * T'].
+
+Canonical finClatticeType
+          (T : finCLatticeType disp1) (T' : finCLatticeType disp2) :=
+  [finCLatticeType of T * T'].
+
+End ProductOrder.
+
+Module Exports.
+Canonical porderType.
+Canonical latticeType.
+Canonical blatticeType.
+Canonical tblatticeType.
+Canonical cblatticeType.
+Canonical ctblatticeType.
+Canonical finPOrderType.
+Canonical finLatticeType.
+Canonical finClatticeType.
+End Exports.
+End ProductOrder.
+
+Module ProdLexOrder.
+Section ProdLexOrder.
+Context {disp1 disp2 disp3 : unit}.
+
+Section POrder.
+Variable (T : porderType disp1) (T' : porderType disp2).
+Implicit Types (x y : T * T').
+
+Definition le x y := (x.1 <= y.1) && ((x.1 >= y.1) ==> (x.2 <= y.2)).
+
+Fact refl : reflexive le.
+Proof. by move=> ?; by rewrite /le !lexx. Qed.
 
+Fact anti : antisymmetric le.
+Proof.
+rewrite /le => -[x x'] [y y'] /=; case_eq (y <= x); case_eq (x <= y) => //.
+by move=> //= hxy hyx /le_anti ->; move/andP/le_anti: (conj hxy hyx) => ->.
+Qed.
+
+Fact trans : transitive le.
+Proof.
+move=> y x z /andP [hxy /implyP hxy'] /andP [hyz /implyP hyz'].
+rewrite /le (le_trans hxy) //=; apply/implyP => hzx.
+by apply/le_trans/hxy'/(le_trans hyz): (hyz' (le_trans hzx hxy)).
+Qed.
+
+Definition porderMixin := LePOrderMixin refl anti trans (rrefl _).
+Canonical porderType := POrderType disp3 (T * T') porderMixin.
+
+End POrder.
+
+Section Total.
+Variable (T : orderType disp1) (T' : orderType disp2).
+Implicit Types (x y : T * T').
+
+Fact total : totalLatticeMixin [porderType of T * T'].
+Proof.
+move=> x y; rewrite /POrderDef.le /= /le; case: (ltgtP x.1 y.1) => _ //=.
+by apply: le_total.
+Qed.
+
+Canonical latticeType := LatticeType (T * T') total.
+Canonical totalType := LatticeType (T * T') total.
+
+End Total.
+
+End ProdLexOrder.
+
+Module Exports.
+Canonical porderType.
+Canonical latticeType.
+Canonical totalType.
+End Exports.
+End ProdLexOrder.
+
+Module SeqProdOrder.
+Section SeqProdOrder.
+Context {disp disp' : unit}.
+
+Section POrder.
+Variable T : porderType disp.
 Implicit Types s : seq T.
 
-Fixpoint lexi s1 s2 :=
+Fixpoint le s1 s2 :=
+  if s1 is x1 :: s1' then
+    if s2 is x2 :: s2' then (x1 <= x2) && le s1' s2' else false
+  else
+    true.
+
+Fact refl : reflexive le.
+Proof. by elim=> //= ? ? ?; rewrite !lexx. Qed.
+
+Fact anti : antisymmetric le.
+Proof.
+elim=> [|? ? ih] [|? ?] //=.
+by rewrite andbAC andbA andbAC -andbA => /andP [] /le_anti -> /ih ->.
+Qed.
+
+Fact trans : transitive le.
+Proof.
+elim=> [|y ys ih] [|x xs] [|z zs] //=.
+by case/andP => [] xy xys /andP [] /(le_trans xy) -> /(ih _ _ xys).
+Qed.
+
+Definition porderMixin := LePOrderMixin refl anti trans (rrefl _).
+Canonical porderType := POrderType disp' (seq T) porderMixin.
+
+End POrder.
+
+Section BLattice.
+Variable T : latticeType disp.
+Implicit Types s : seq T.
+
+Fixpoint meet s1 s2 :=
+  match s1, s2 with
+    | x1 :: s1', x2 :: s2' => (x1 `&` x2) :: meet s1' s2'
+    | _, _ => [::]
+  end.
+
+Fixpoint join s1 s2 :=
+  match s1, s2 with
+    | [::], _ => s2
+    | _, [::] => s1
+    | x1 :: s1', x2 :: s2' => (x1 `|` x2) :: join s1' s2'
+  end.
+
+Fact meetC : commutative meet.
+Proof. by elim=> [|? ? ih] [|? ?] //=; rewrite meetC ih. Qed.
+
+Fact joinC : commutative join.
+Proof. by elim=> [|? ? ih] [|? ?] //=; rewrite joinC ih. Qed.
+
+Fact meetA : associative meet.
+Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite meetA ih. Qed.
+
+Fact joinA : associative join.
+Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite joinA ih. Qed.
+
+Fact meetss s : meet s s = s.
+Proof. by elim: s => [|? ? ih] //=; rewrite meetxx ih. Qed.
+
+Fact joinKI y x : meet x (join x y) = x.
+Proof.
+elim: x y => [|? ? ih] [|? ?] //=; rewrite (meetxx, joinKI) ?ih //.
+by congr cons; rewrite meetss.
+Qed.
+
+Fact meetKU y x : join x (meet x y) = x.
+Proof. by elim: x y => [|? ? ih] [|? ?] //=; rewrite meetKU ih. Qed.
+
+Fact leEmeet x y : (x <= y) = (meet x y == x).
+Proof.
+rewrite /POrderDef.le /=.
+by elim: x y => [|? ? ih] [|? ?] //=; rewrite /eq_op /= leEmeet ih.
+Qed.
+
+Fact meetUl : left_distributive meet join.
+Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite meetUl ih. Qed.
+
+Fact le0x s : [::] <= s.
+Proof. by []. Qed.
+
+Definition latticeMixin :=
+  Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+Canonical latticeType := LatticeType (seq T) latticeMixin.
+Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin le0x).
+
+End BLattice.
+
+End SeqProdOrder.
+
+Module Exports.
+Canonical porderType.
+Canonical latticeType.
+Canonical blatticeType.
+End Exports.
+End SeqProdOrder.
+
+Module SeqLexOrder.
+Section SeqLexOrder.
+Context {disp : unit}.
+
+Section POrder.
+Variable T : porderType disp.
+Implicit Types s : seq T.
+
+Fixpoint le s1 s2 :=
   if s1 is x1 :: s1' then
     if s2 is x2 :: s2' then
-      (x1 < x2) || ((x1 == x2) && lexi s1' s2')
+      (x1 < x2) || (x1 == x2) && le s1' s2'
     else
       false
   else
     true.
 
-Fact lexi_le_head x sx y sy:
-  lexi (x :: sx) (y :: sy) -> x <= y.
-Proof. by case/orP => [/ltW|/andP [/eqP-> _]]. Qed.
-
-Fact lexi_refl: reflexive lexi.
+Fact refl: reflexive le.
 Proof. by elim => [|x s ih] //=; rewrite eqxx ih orbT. Qed.
 
-Fact lexi_anti: antisymmetric lexi.
+Fact anti: antisymmetric le.
 Proof.
 move=> x y /andP []; elim: x y => [|x sx ih] [|y sy] //=.
 by case: comparableP => //= -> lesxsy /(ih _ lesxsy) ->.
 Qed.
 
-Fact lexi_trans: transitive lexi.
+Fact trans: transitive le.
 Proof.
 elim=> [|y sy ih] [|x sx] [|z sz] //=.
 case: (comparableP x y) => //=; case: (comparableP y z) => //=.
@@ -2798,17 +3630,49 @@ case: (comparableP x y) => //=; case: (comparableP y z) => //=.
 - by move=> ltyz /lt_trans - /(_ _ ltyz) ->.
 Qed.
 
-Definition lexi_porderMixin := LePOrderMixin lexi_refl lexi_anti lexi_trans.
-Canonical lexi_porderType := POrderType display (seq T) lexi_porderMixin.
+Definition porderMixin := LePOrderMixin refl anti trans (rrefl _).
+Canonical porderType := POrderType disp (seq T) porderMixin.
+
+Fact lexi_le_head x sx y sy: x :: sx <= y :: sy -> x <= y.
+Proof. by case/orP => [/ltW|/andP [/eqP-> _]]. Qed.
+
+End POrder.
+
+Section Total.
+Variable T : orderType disp.
+Implicit Types s : seq T.
+
+Fact total : totalLatticeMixin [porderType of seq T].
+Proof.
+rewrite /totalLatticeMixin /= /POrderDef.le /=.
+by elim=> [|? ? ih] [|? ?] //=;case: ltgtP => //=.
+Qed.
+
+Fact le0x s : [::] <= s.
+Proof. by []. Qed.
+
+Canonical latticeType := LatticeType (seq T) total.
+Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin le0x).
+Canonical totalType := LatticeType (seq T) total.
+
+End Total.
 
-End SeqLexPOrder.
-End SeqLexPOrder.
+End SeqLexOrder.
 
-Canonical SeqLexPOrder.lexi_porderType.
+Module Exports.
+Canonical porderType.
+Canonical latticeType.
+Canonical blatticeType.
+Canonical totalType.
+Definition lexi_le_head := @lexi_le_head.
+Arguments lexi_le_head {disp}.
+End Exports.
+End SeqLexOrder.
 
 Module Def.
 Export POrderDef.
 Export LatticeDef.
+Export TotalDef.
 Export BLatticeDef.
 Export TBLatticeDef.
 Export CBLatticeDef.
@@ -2817,43 +3681,58 @@ End Def.
 
 Module Syntax.
 Export POSyntax.
+Export TotalSyntax.
 Export LatticeSyntax.
 Export BLatticeSyntax.
 Export TBLatticeSyntax.
 Export CBLatticeSyntax.
 Export CTBLatticeSyntax.
-Export ReverseSyntax.
+Export ConverseSyntax.
 End Syntax.
 
-Module Theory.
-Export ReversePOrder.
+Module LTheory.
+Export POCoercions.
+Export ConversePOrder.
 Export POrderTheory.
-Export TotalTheory.
-Export ReverseLattice.
+
+Export ConverseLattice.
 Export LatticeTheoryMeet.
 Export LatticeTheoryJoin.
 Export BLatticeTheory.
-Export CBLatticeTheory.
-Export ReverseTBLattice.
+Export ConverseTBLattice.
 Export TBLatticeTheory.
-Export CTBLatticeTheory.
-Export NatOrder.
-Export SeqLexPOrder.
+End LTheory.
 
-Export POrder.Exports.
-Export Total.Exports.
-Export Lattice.Exports.
-Export BLattice.Exports.
-Export CBLattice.Exports.
-Export TBLattice.Exports.
-Export CTBLattice.Exports.
-Export FinPOrder.Exports.
-Export FinTotal.Exports.
-Export FinLattice.Exports.
-Export FinBLattice.Exports.
-Export FinCBLattice.Exports.
-Export FinTBLattice.Exports.
-Export FinCTBLattice.Exports.
+Module CTheory.
+Export LTheory CBLatticeTheory CTBLatticeTheory.
+End CTheory.
+
+Module TTheory.
+Export LTheory TotalTheory.
+End TTheory.
+
+Module Theory.
+Export CTheory TotalTheory.
 End Theory.
 
 End Order.
+
+Export Order.POrder.Exports.
+Export Order.FinPOrder.Exports.
+Export Order.Lattice.Exports.
+Export Order.BLattice.Exports.
+Export Order.TBLattice.Exports.
+Export Order.FinLattice.Exports.
+Export Order.CBLattice.Exports.
+Export Order.CTBLattice.Exports.
+Export Order.FinCLattice.Exports.
+Export Order.Total.Exports.
+Export Order.FinTotal.Exports.
+
+Export Order.TotalLatticeMixin.Exports.
+Export Order.LePOrderMixin.Exports.
+Export Order.LtPOrderMixin.Exports.
+Export Order.MeetJoinMixin.Exports.
+Export Order.LeOrderMixin.Exports.
+Export Order.LtOrderMixin.Exports.
+Export Order.NatOrder.Exports.