Initial import of order.v into mathcomp

1 files changed, 2859 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
new file mode 100644
index 0000000..cd8d8d8
--- /dev/null
+++ b/mathcomp/ssreflect/order.v
@@ -0,0 +1,2859 @@
+(*************************************************************************)
+(* Copyright (C) 2012 - 2016 (Draft)                                     *)
+(* C. Cohen                                                              *)
+(* Based on prior works by                                               *)
+(* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani            *)
+(*                                                                       *)
+(* This program is free software: you can redistribute it and/or modify  *)
+(* it under the terms of the GNU General Public License as published by  *)
+(* the Free Software Foundation, either version 3 of the License, or     *)
+(* (at your option) any later version.                                   *)
+(*                                                                       *)
+(* This program is distributed in the hope that it will be useful,       *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(* GNU General Public License for more details.                          *)
+(*                                                                       *)
+(* 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 (<).                                *)
+(*****************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Delimit Scope order_scope with O.
+Local Open Scope order_scope.
+
+Reserved Notation "<= y" (at level 35).
+Reserved Notation ">= y" (at level 35).
+Reserved Notation "< y" (at level 35).
+Reserved Notation "> y" (at level 35).
+Reserved Notation "<= y :> T" (at level 35, y at next level).
+Reserved Notation ">= y :> T" (at level 35, y at next level).
+Reserved Notation "< y :> T" (at level 35, y at next level).
+Reserved Notation "> y :> T" (at level 35, y at next level).
+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 >< 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 for lattice operations. *)
+Reserved Notation "A `&` B"  (at level 48, left associativity).
+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 "\meet_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \meet_ i '/  '  F ']'").
+Reserved Notation "\meet_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \meet_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\meet_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \meet_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\meet_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \meet_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\meet_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \meet_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\meet_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \meet_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\meet_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\meet_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\meet_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \meet_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\meet_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \meet_ ( i  <  n )  F ']'").
+Reserved Notation "\meet_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \meet_ ( i  'in'  A  |  P ) '/  '  F ']'").
+Reserved Notation "\meet_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \meet_ ( i  'in'  A ) '/  '  F ']'").
+
+Reserved Notation "\join_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \join_ i '/  '  F ']'").
+Reserved Notation "\join_ ( i <- r | P ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \join_ ( i  <-  r  |  P ) '/  '  F ']'").
+Reserved Notation "\join_ ( i <- r ) F"
+  (at level 41, F at level 41, i, r at level 50,
+           format "'[' \join_ ( i  <-  r ) '/  '  F ']'").
+Reserved Notation "\join_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \join_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\join_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \join_ ( m  <=  i  <  n ) '/  '  F ']'").
+Reserved Notation "\join_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \join_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\join_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\join_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\join_ ( i < n | P ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \join_ ( i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\join_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \join_ ( i  <  n )  F ']'").
+Reserved Notation "\join_ ( i 'in' A | P ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \join_ ( i  'in'  A  |  P ) '/  '  F ']'").
+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"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \meet^r_ i '/  '  F ']'").
+Reserved Notation "\meet^r_ ( 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"
+  (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"
+  (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"
+  (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"
+  (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"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\meet^r_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\meet^r_ ( 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"
+  (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"
+  (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"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \meet^r_ ( i  'in'  A ) '/  '  F ']'").
+
+Reserved Notation "\join^r_ 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"
+  (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"
+  (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"
+  (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"
+  (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"
+  (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"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\join^r_ ( i : t ) F"
+  (at level 41, F at level 41, i at level 50,
+           only parsing).
+Reserved Notation "\join^r_ ( 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"
+  (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"
+  (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"
+  (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.
+
+Module Order.
+
+(**************)
+(* STRUCTURES *)
+(**************)
+
+Module POrder.
+Section ClassDef.
+Structure mixin_of (T : eqType) := Mixin {
+  le : rel T;
+  lt : rel T;
+  _  : forall x y, lt x y = (x != y) && (le x y);
+  _  : reflexive     le;
+  _  : antisymmetric le;
+  _  : transitive    le
+}.
+
+Record class_of T := Class {
+  base  : Choice.class_of T;
+  mixin : mixin_of (EqType T base)
+}.
+
+Local Coercion base : class_of >-> Choice.class_of.
+
+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.
+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 =>
+  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.
+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)
+  (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.
+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]
+  (at level 0, format "[ 'porderType'  'of'  T  'with' disp ]") : form_scope.
+End Exports.
+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 (T : porderType).
+
+Definition le (R : porderType) : rel R := POrder.le (POrder.class R).
+Local Notation "x <= y" := (le x y) : order_scope.
+
+Definition lt (R : porderType) : rel R := POrder.lt (POrder.class R).
+Local Notation "x < y" := (lt x y) : order_scope.
+
+Definition comparable (R : porderType) : rel R :=
+  fun (x y : R) => (x <= y) || (y <= x).
+Local Notation "x >=< y" := (comparable x y) : order_scope.
+Local Notation "x >< y" := (~~ (x >=< y)) : order_scope.
+
+Definition ge : simpl_rel T := [rel x y | y <= x].
+Definition gt : simpl_rel T := [rel x y | y < x].
+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 :=
+  | 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 :=
+  | 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) :
+  bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | ComparerEq of x = y : comparer x y
+    true true true true false false
+  | ComparerLt of x < y : comparer x y
+    false false true false true false
+  | ComparerGt of y < x : comparer x y
+    false false false true false true.
+
+CoInductive 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
+  | InComparerLt of x < y : incomparer x y
+    false false true false true false true true
+  | InComparerGt of y < x : incomparer x y
+    false false false true false true true true
+  | InComparer of x >< y : incomparer x y
+    false false false false false false false false.
+
+End Def.
+End POrderDef.
+
+Prenex Implicits lt le leif.
+Arguments ge {_ _}.
+Arguments gt {_ _}.
+
+Module Import POSyntax.
+
+Notation "<=%O" := le : order_scope.
+Notation ">=%O" := ge : order_scope.
+Notation "<%O" := lt : order_scope.
+Notation ">%O" := gt : order_scope.
+Notation "<?=%O" := leif : order_scope.
+Notation ">=<%O" := comparable : order_scope.
+Notation "><%O" := (fun x y => ~~ (comparable x y)) : order_scope.
+
+Notation "<= y" := (ge y) : order_scope.
+Notation "<= y :> T" := (<= (y : T)) : order_scope.
+Notation ">= y"  := (le y) : order_scope.
+Notation ">= y :> T" := (>= (y : T)) : order_scope.
+
+Notation "< y" := (gt y) : order_scope.
+Notation "< y :> T" := (< (y : T)) : order_scope.
+Notation "> y" := (lt y) : order_scope.
+Notation "> y :> T" := (> (y : T)) : order_scope.
+
+Notation ">=< y" := (comparable y) : order_scope.
+Notation ">=< y :> T" := (>=< (y : T)) : order_scope.
+
+Notation "x <= y" := (le x y) : order_scope.
+Notation "x <= y :> T" := ((x : T) <= (y : T)) : order_scope.
+Notation "x >= y" := (y <= x) (only parsing) : order_scope.
+Notation "x >= y :> T" := ((x : T) >= (y : T)) (only parsing) : order_scope.
+
+Notation "x < y"  := (lt x y) : order_scope.
+Notation "x < y :> T" := ((x : T) < (y : T)) : order_scope.
+Notation "x > y"  := (y < x) (only parsing) : order_scope.
+Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : order_scope.
+
+Notation "x <= y <= z" := ((x <= y) && (y <= z)) : order_scope.
+Notation "x < y <= z" := ((x < y) && (y <= z)) : order_scope.
+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)
+  (only parsing) : order_scope.
+
+Notation ">=< x" := (comparable x) : order_scope.
+Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope.
+Notation "x >=< y" := (comparable x y) : order_scope.
+
+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 Lattice.
+Section ClassDef.
+
+Structure mixin_of d (T : porderType d) := Mixin {
+  meet : T -> T -> T;
+  join : T -> T -> T;
+  _ : commutative meet;
+  _ : commutative join;
+  _ : associative meet;
+  _ : associative join;
+  _ : forall y x, meet x (join x y) = x;
+  _ : forall y x, join x (meet x y) = x;
+  _ : forall x y, (x <= y) = (meet x y == x);
+  _ : left_distributive meet join;
+}.
+
+Record class_of d (T : Type) := Class {
+  base  : POrder.class_of T;
+  mixin : mixin_of (POrder.Pack d base)
+}.
+
+Local Coercion base : class_of >-> POrder.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.
+Definition clone disp' c of (disp = disp') & phant_id class c :=
+  @Pack disp' T c.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+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.
+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)
+  (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.
+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]
+  (at level 0, format "[ 'latticeType'  'of'  T  'with' disp ]") : form_scope.
+End Exports.
+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).
+End LatticeDef.
+End LatticeDef.
+
+Module Import LatticeSyntax.
+
+Notation "x `&` y" :=  (meet x y).
+Notation "x `|` y" := (join x y).
+
+End LatticeSyntax.
+
+Module Total.
+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))
+}.
+
+Local Coercion base : class_of >-> Lattice.class_of.
+
+Structure type d := Pack { sort; _ : class_of d 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.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+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 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)
+  (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.
+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]
+  (at level 0, format "[ 'orderType'  'of'  T  'with' disp ]") : form_scope.
+
+End Exports.
+End Total.
+
+Import Total.Exports.
+
+Module BLattice.
+Section ClassDef.
+Structure 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)
+}.
+
+Local Coercion base : class_of >-> Lattice.class_of.
+
+Structure type d := Pack { sort; _ : class_of d 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.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+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.
+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)
+  (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.
+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]
+  (at level 0, format "[ 'blatticeType'  'of'  T  'with' disp ]") : form_scope.
+End Exports.
+End BLattice.
+
+Export BLattice.Exports.
+
+Module Import BLatticeDef.
+Definition bottom {disp : unit} {T : blatticeType disp} : T :=
+  BLattice.bottom (BLattice.class T).
+End BLatticeDef.
+
+Module Import BLatticeSyntax.
+Notation "0" := bottom : order_scope.
+
+Notation "\join_ ( i <- r | P ) F" :=
+  (\big[@join _ _/0%O]_(i <- r | P%B) F%O) : order_scope.
+Notation "\join_ ( i <- r ) F" :=
+  (\big[@join _ _/0%O]_(i <- r) F%O) : order_scope.
+Notation "\join_ ( i | P ) F" :=
+  (\big[@join _ _/0%O]_(i | P%B) F%O) : order_scope.
+Notation "\join_ i F" :=
+  (\big[@join _ _/0%O]_i F%O) : order_scope.
+Notation "\join_ ( i : I | P ) F" :=
+  (\big[@join _ _/0%O]_(i : I | P%B) F%O) (only parsing) : order_scope.
+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.
+Notation "\join_ ( m <= i < n ) F" :=
+ (\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.
+Notation "\join_ ( i < n ) F" :=
+ (\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.
+Notation "\join_ ( i 'in' A ) F" :=
+ (\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 {
+  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)
+}.
+
+Local Coercion base : class_of >-> BLattice.class_of.
+
+Structure type d := Pack { sort; _ : class_of d 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.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition porderType := @POrder.Pack disp cT xclass.
+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.
+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)
+  (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.
+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]
+  (at level 0, format "[ 'tblatticeType'  'of'  T  'with' disp ]") : form_scope.
+
+End Exports.
+End TBLattice.
+
+Export TBLattice.Exports.
+
+Module Import TBLatticeDef.
+Definition top disp  {T : tblatticeType disp} : T :=
+  TBLattice.top (TBLattice.class T).
+End TBLatticeDef.
+
+Module Import TBLatticeSyntax.
+
+Notation "1" := top : order_scope.
+
+Notation "\meet_ ( i <- r | P ) F" :=
+  (\big[meet/1]_(i <- r | P%B) F%O) : order_scope.
+Notation "\meet_ ( i <- r ) F" :=
+  (\big[meet/1]_(i <- r) F%O) : order_scope.
+Notation "\meet_ ( i | P ) F" :=
+  (\big[meet/1]_(i | P%B) F%O) : order_scope.
+Notation "\meet_ i F" :=
+  (\big[meet/1]_i F%O) : order_scope.
+Notation "\meet_ ( i : I | P ) F" :=
+  (\big[meet/1]_(i : I | P%B) F%O) (only parsing) : order_scope.
+Notation "\meet_ ( i : I ) F" :=
+  (\big[meet/1]_(i : I) F%O) (only parsing) : order_scope.
+Notation "\meet_ ( m <= i < n | P ) F" :=
+ (\big[meet/1]_(m <= i < n | P%B) F%O) : order_scope.
+Notation "\meet_ ( m <= i < n ) F" :=
+ (\big[meet/1]_(m <= i < n) F%O) : order_scope.
+Notation "\meet_ ( i < n | P ) F" :=
+ (\big[meet/1]_(i < n | P%B) F%O) : order_scope.
+Notation "\meet_ ( i < n ) F" :=
+ (\big[meet/1]_(i < n) F%O) : order_scope.
+Notation "\meet_ ( i 'in' A | P ) F" :=
+ (\big[meet/1]_(i in A | P%B) F%O) : order_scope.
+Notation "\meet_ ( i 'in' A ) F" :=
+ (\big[meet/1]_(i in A) F%O) : order_scope.
+
+End TBLatticeSyntax.
+
+Module CBLattice.
+Section ClassDef.
+Structure 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)
+}.
+
+Local Coercion base : class_of >-> BLattice.class_of.
+
+Structure type d := Pack { sort; _ : class_of d 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.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition porderType := @POrder.Pack disp cT xclass.
+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.
+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)
+  (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.
+
+End Exports.
+End CBLattice.
+
+Export CBLattice.Exports.
+
+Module Import CBLatticeDef.
+Definition sub {disp : unit} {T : cblatticeType disp} : T -> T -> T :=
+  CBLattice.sub (CBLattice.class T).
+End CBLatticeDef.
+
+Module Import CBLatticeSyntax.
+Notation "x `\` y" := (sub x y).
+End CBLatticeSyntax.
+
+Module CTBLattice.
+Section ClassDef.
+Record mixin_of d (T : tblatticeType d) (sub : T -> T -> T) := Mixin {
+   compl : T -> T;
+   _ : 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)
+}.
+
+Local Coercion base : class_of >-> TBLattice.class_of.
+Local Coercion base2 d T (c : class_of d T) :=
+  CBLattice.Class (mixin1 c).
+
+Structure type d := Pack { sort; _ : class_of d 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.
+Let xT := let: Pack T _ := cT in T.
+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).
+
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition porderType := @POrder.Pack disp cT xclass.
+Definition latticeType := @Lattice.Pack disp cT xclass.
+Definition blatticeType := @BLattice.Pack disp cT xclass.
+Definition tblatticeType := @TBLattice.Pack disp cT xclass.
+Definition cblatticeType := @CBLattice.Pack disp cT xclass.
+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.
+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.
+Canonical latticeType.
+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 "[ 'default_ctblatticeType' 'of' T ]" :=
+  (@pack T _ _ _ id _ _ id (fun=> erefl))
+  (at level 0, format "[ 'default_ctblatticeType'  'of'  T ]") : form_scope.
+
+End Exports.
+End CTBLattice.
+
+Export CTBLattice.Exports.
+
+Module Import CTBLatticeDef.
+Definition compl {d : unit} {T : ctblatticeType d} : T -> T :=
+  CTBLattice.compl (CTBLattice.class T).
+End CTBLatticeDef.
+
+Module Import CTBLatticeSyntax.
+Notation "~` A" := (compl A).
+End CTBLatticeSyntax.
+
+(**********)
+(* FINITE *)
+(**********)
+
+Module FinPOrder.
+Section ClassDef.
+
+Record class_of T := Class {
+  base  : Finite.class_of T;
+  mixin : POrder.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.
+
+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.
+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 =>
+  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 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.
+Coercion eqType : type >-> Equality.type.
+Coercion finType : type >-> Finite.type.
+Coercion choiceType : type >-> Choice.type.
+Coercion porderType : type >-> POrder.type.
+
+Canonical eqType.
+Canonical finType.
+Canonical choiceType.
+Canonical porderType.
+Canonical fin_porderType.
+
+Notation finPOrderType := type.
+Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id  _ _ phant_id)
+  (at level 0, format "[ 'finPOrderType'  'of'  T ]") : form_scope.
+
+End Exports.
+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)
+}.
+
+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.
+
+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 (@BLattice.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 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 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.
+
+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.
+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.
+Coercion finBLatticeType : type >-> FinBLattice.type.
+Coercion tblatticeType : type >-> TBLattice.type.
+
+Canonical eqType.
+Canonical finType.
+Canonical choiceType.
+Canonical porderType.
+Canonical finPOrderType.
+Canonical latticeType.
+Canonical finLatticeType.
+Canonical blatticeType.
+Canonical finBLatticeType.
+Canonical tblatticeType.
+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.
+End Exports.
+End FinTBLattice.
+
+Export FinTBLattice.Exports.
+
+Module FinCBLattice.
+Section ClassDef.
+
+Record class_of d (T : Type) := Class {
+  base  : FinBLattice.class_of d T;
+  mixin : CBLattice.mixin_of (BLattice.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.
+
+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 (@CBLattice.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 blatticeType := @BLattice.Pack disp cT xclass.
+Definition finBLatticeType := @FinBLattice.Pack disp cT xclass.
+Definition cblatticeType := @CBLattice.Pack disp cT xclass.
+Definition fin_blatticeType := @CBLattice.Pack disp finBLatticeType 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.
+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.
+Coercion finBLatticeType : type >-> FinBLattice.type.
+Coercion cblatticeType : type >-> CBLattice.type.
+
+Canonical eqType.
+Canonical finType.
+Canonical choiceType.
+Canonical porderType.
+Canonical finPOrderType.
+Canonical latticeType.
+Canonical finLatticeType.
+Canonical blatticeType.
+Canonical finBLatticeType.
+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.
+End Exports.
+End FinCBLattice.
+
+Export FinCBLattice.Exports.
+
+Module FinCTBLattice.
+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)
+}.
+
+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.
+
+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 (@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 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 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.
+
+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.
+
+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.
+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.
+
+
+Canonical eqType.
+Canonical finType.
+Canonical choiceType.
+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.
+End Exports.
+End FinCTBLattice.
+
+Export FinCTBLattice.Exports.
+
+(***********)
+(* REVERSE *)
+(***********)
+
+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.
+
+Module Import ReverseSyntax.
+
+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)) :
+  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 "<^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 ">=<^r y" := (>=<^r%O y) : order_scope.
+Notation ">=<^r y :> T" := (>=<^r (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 <^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 <=^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 <=^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)
+  (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 "><^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 "x `&^r` y" :=  (@meet (reverse_display _) _ x y).
+Notation "x `|^r` y" := (@join (reverse_display _) _ x y).
+
+End ReverseSyntax.
+
+(**********)
+(* THEORY *)
+(**********)
+
+Module Import POrderTheory.
+Section POrderTheory.
+
+Context {display : unit}.
+Local Notation porderType := (porderType display).
+Context {T : porderType}.
+
+Implicit Types x y : T.
+
+Lemma lexx (x : T) : x <= x.
+Proof. by case: T x => ? [? []]. Qed.
+Hint Resolve lexx.
+
+Definition le_refl : reflexive le := lexx.
+Hint Resolve le_refl.
+
+Lemma le_anti: antisymmetric (<=%O : rel T).
+Proof. by case: T => ? [? []]. Qed.
+
+Lemma le_trans: transitive (<=%O : rel T).
+Proof. by case: T => ? [? []]. Qed.
+
+Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y).
+Proof. by case: T x y => ? [? []]. Qed.
+
+Lemma ltxx x: x < x = false.
+Proof. by rewrite lt_neqAle eqxx. Qed.
+
+Definition lt_irreflexive : irreflexive lt := ltxx.
+Hint Resolve lt_irreflexive.
+
+Lemma le_eqVlt x y: (x <= y) = (x == y) || (x < y).
+Proof. by rewrite lt_neqAle; case: eqP => //= ->; rewrite lexx. Qed.
+
+Lemma lt_eqF x y: x < y -> x == y = false.
+Proof. by rewrite lt_neqAle => /andP [/negbTE->]. Qed.
+
+Lemma gt_eqF x y : y < x -> x == y = false.
+Proof. by apply: contraTF => /eqP ->; rewrite ltxx. Qed.
+
+Lemma eq_le x y: (x == y) = (x <= y <= x).
+Proof. by apply/eqP/idP => [->|/le_anti]; rewrite ?lexx. Qed.
+
+Lemma ltW x y: x < y -> x <= y.
+Proof. by rewrite le_eqVlt orbC => ->. Qed.
+
+Lemma lt_le_trans y x z: x < y -> y <= z -> x < z.
+Proof.
+rewrite !lt_neqAle => /andP [nexy lexy leyz]; rewrite (le_trans lexy) // andbT.
+by apply: contraNneq nexy => eqxz; rewrite eqxz eq_le leyz andbT in lexy *.
+Qed.
+
+Lemma lt_trans: transitive (<%O : rel T).
+Proof. by move=> y x z le1 /ltW le2; apply/(@lt_le_trans y). Qed.
+
+Lemma le_lt_trans y x z: x <= y -> y < z -> x < z.
+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 le_gtF x y: x <= y -> y < x = false.
+Proof.
+by move=> le_xy; apply/negP => /lt_le_trans /(_ le_xy); rewrite ltxx.
+Qed.
+
+Lemma lt_geF x y : (x < y) -> y <= x = false.
+Proof.
+by move=> le_xy; apply/negP => /le_lt_trans /(_ le_xy); rewrite ltxx.
+Qed.
+
+Definition lt_gtF x y hxy := le_gtF (@ltW x y hxy).
+
+Lemma lt_leAnge x y : (x < y) = (x <= y) && ~~ (y <= x).
+Proof.
+apply/idP/idP => [ltxy|/andP[lexy Nleyx]]; first by rewrite ltW // lt_geF.
+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.
+
+Lemma le_lt_asym x y : x <= y < x = false.
+Proof. by rewrite andbC lt_le_asym. Qed.
+
+Lemma lt_sorted_uniq_le (s : seq T) :
+   sorted lt s = uniq s && sorted le s.
+Proof.
+case: s => //= n s; elim: s n => //= m s IHs n.
+rewrite inE lt_neqAle negb_or IHs -!andbA.
+case sn: (n \in s); last do !bool_congr.
+rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm.
+by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)).
+Qed.
+
+Lemma eq_sorted_lt (s1 s2 : seq T) :
+  sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2.
+Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed.
+
+Lemma eq_sorted_le (s1 s2 : seq T) :
+   sorted le s1 -> sorted le s2 -> perm_eq s1 s2 -> s1 = s2.
+Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed.
+
+Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x).
+Proof.
+move=> c_xy; apply/idP/idP => [/le_gtF/negP/negP//|]; rewrite lt_neqAle.
+by move: c_xy => /orP [] -> //; rewrite andbT negbK => /eqP ->.
+Qed.
+
+Lemma comparable_ltNge x y : x >=< y -> (x < y) = ~~ (y <= x).
+Proof.
+move=> c_xy; apply/idP/idP => [/lt_geF/negP/negP//|].
+by rewrite lt_neqAle eq_le; move: c_xy => /orP [] -> //; rewrite andbT.
+Qed.
+
+Lemma comparable_ltgtP x y : x >=< y ->
+  comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y).
+Proof.
+rewrite />=<%O !le_eqVlt [y == x]eq_sym.
+have := (altP (x =P y), (boolP (x < y), boolP (y < x))).
+move=> [[->//|neq_xy /=] [[] xy [] //=]] ; do ?by rewrite ?ltxx; constructor.
+  by rewrite ltxx in xy.
+by rewrite le_gtF // ltW.
+Qed.
+
+Lemma comparable_leP x y : x >=< y -> le_xor_gt x y (x <= y) (y < x).
+Proof.
+by move=> /comparable_ltgtP [->|xy|xy]; constructor => //; rewrite ltW.
+Qed.
+
+Lemma comparable_ltP x y : x >=< y -> lt_xor_ge x y (y <= x) (x < y).
+Proof.
+by move=> /comparable_ltgtP [->|xy|xy]; constructor => //; rewrite ltW.
+Qed.
+
+Lemma comparable_sym x y : (y >=< x) = (x >=< y).
+Proof. by rewrite /comparable orbC. Qed.
+
+Lemma comparablexx x : x >=< x.
+Proof. by rewrite /comparable lexx. Qed.
+
+Lemma incomparable_eqF x y : (x >< y) -> (x == y) = false.
+Proof. by apply: contraNF => /eqP ->; rewrite comparablexx. Qed.
+
+Lemma incomparable_leF x y : (x >< y) -> (x <= y) = false.
+Proof. by apply: contraNF; rewrite /comparable => ->. Qed.
+
+Lemma incomparable_ltF x y : (x >< y) -> (x < y) = false.
+Proof. by rewrite lt_neqAle => /incomparable_leF ->; rewrite andbF. Qed.
+
+Lemma comparableP x y : incomparer x y
+  (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y)
+  (y >=< x) (x >=< y).
+Proof.
+rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y).
+  by case: (comparable_ltgtP c_xy) => ?; constructor.
+by rewrite ?incomparable_eqF ?incomparable_leF ?incomparable_ltF //
+           1?comparable_sym //; constructor.
+Qed.
+
+Lemma le_comparable (x y : T) : x <= y -> x >=< y.
+Proof. by case: comparableP. Qed.
+
+Lemma lt_comparable (x y : T) : x < y -> x >=< y.
+Proof. by case: comparableP. Qed.
+
+Lemma ge_comparable (x y : T) : y <= x -> x >=< y.
+Proof. by case: comparableP. Qed.
+
+Lemma gt_comparable (x y : T) : y < x -> x >=< y.
+Proof. by case: comparableP. Qed.
+
+Lemma leifP x y C : reflect (x <= y ?= iff C) (if C then x == y else x < y).
+Proof.
+rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]].
+  by case: C => [/eqP->|lxy]; rewrite ?eqxx // lxy lt_eqF.
+by move=> /orP[/eqP->|lxy] <-; rewrite ?eqxx // lt_eqF.
+Qed.
+
+End POrderTheory.
+End POrderTheory.
+
+Hint Resolve lexx le_refl lt_irreflexive.
+
+
+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].
+
+Context {display : unit}.
+Local Notation porderType := (porderType display).
+Variable T : porderType.
+
+Definition reverse_le (x y : T) := (y <= x).
+Definition reverse_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.
+
+Fact reverse_le_anti : antisymmetric reverse_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
+             (fun y z x zy yx => @le_trans _ _ y x z yx zy).
+Canonical reverse_porderType :=
+  POrderType (reverse_display display) (T^r) reverse_porderMixin.
+
+End ReversePOrder.
+End ReversePOrder.
+
+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).
+
+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 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 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.
+
+Lemma meetUK x y : (x `&` y) `|` y = y.
+Proof. by rewrite joinC meetC meetKU. Qed.
+Lemma joinIK x y : (x `|` y) `&` y = y.
+Proof. by rewrite joinC meetC joinKI. Qed.
+
+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.
+
+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.
+
+Lemma meetUr : right_distributive (@meet _ L) (@join _ L).
+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).
+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.
+
+Module Import LatticeTheoryMeet.
+Section LatticeTheoryMeet.
+Context {display : unit}.
+Local Notation latticeType := (latticeType display).
+Context {L : latticeType}.
+Implicit Types (x y : L).
+
+(* lattice theory *)
+Lemma meetAC : right_commutative (@meet _ L).
+Proof. by move=> x y z; rewrite -!meetA [X in _ `&` X]meetC. Qed.
+Lemma meetCA : left_commutative (@meet _ L).
+Proof. by move=> x y z; rewrite !meetA [X in X `&` _]meetC. Qed.
+Lemma meetACA : interchange (@meet _ L) (@meet _ L).
+Proof. by move=> x y z t; rewrite !meetA [X in X `&` _]meetAC. Qed.
+
+Lemma meetxx x : x `&` x = x.
+Proof. by rewrite -[X in _ `&` X](meetKU x) joinKI. Qed.
+
+Lemma meetKI y x : x `&` (x `&` y) = x `&` y.
+Proof. by rewrite meetA meetxx. Qed.
+Lemma meetIK y x : (x `&` y) `&` y = x `&` y.
+Proof. by rewrite -meetA meetxx. Qed.
+Lemma meetKIC y x : x `&` (y `&` x) = x `&` y.
+Proof. by rewrite meetC meetIK meetC. Qed.
+Lemma meetIKC y x : y `&` x `&` y = x `&` y.
+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<-]].
+  by rewrite meetA meetIK eqxx -meetA meetACA meetxx meetAC eqxx.
+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 leIr x y : y `&` x <= x.
+Proof. by rewrite leIx ?lexx ?orbT. Qed.
+
+Lemma leIl x y : x `&` y <= x.
+Proof. by rewrite leIx ?lexx ?orbT. 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.
+
+End LatticeTheoryMeet.
+End LatticeTheoryMeet.
+
+Module Import LatticeTheoryJoin.
+Section LatticeTheoryJoin.
+Context {display : unit}.
+Local Notation latticeType := (latticeType display).
+Context {L : latticeType}.
+Implicit Types (x y : L).
+
+(* lattice theory *)
+Lemma joinAC : right_commutative (@join _ L).
+Proof. exact: (@meetAC _ [latticeType of L^r]). Qed.
+Lemma joinCA : left_commutative (@join _ L).
+Proof. exact: (@meetCA _ [latticeType of L^r]). Qed.
+Lemma joinACA : interchange (@join _ L) (@join _ L).
+Proof. exact: (@meetACA _ [latticeType of L^r]). Qed.
+
+Lemma joinxx x : x `|` x = x.
+Proof. exact: (@meetxx _ [latticeType of L^r]). Qed.
+
+Lemma joinKU y x : x `|` (x `|` y) = x `|` y.
+Proof. exact: (@meetKI _ [latticeType of L^r]). Qed.
+Lemma joinUK y x : (x `|` y) `|` y = x `|` y.
+Proof. exact: (@meetIK _ [latticeType of L^r]). Qed.
+Lemma joinKUC y x : x `|` (y `|` x) = x `|` y.
+Proof. exact: (@meetKIC _ [latticeType of L^r]). Qed.
+Lemma joinUKC y x : y `|` x `|` y = x `|` y.
+Proof. exact: (@meetIKC _ [latticeType of L^r]). Qed.
+
+(* interaction with order *)
+Lemma join_idPl {x y} : reflect (x `|` y = y) (x <= y).
+Proof. exact: (@meet_idPr _ [latticeType of L^r]). Qed.
+Lemma join_idPr {x y} : reflect (y `|` x = y) (x <= y).
+Proof. exact: (@meet_idPl _ [latticeType of L^r]). Qed.
+
+Lemma leUidl x y : (x `|` y <= y) = (x <= y).
+Proof. exact: (@leIidr _ [latticeType of L^r]). 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.
+
+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 leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.
+Proof. exact: (@leI2 _ [latticeType of L^r]). Qed.
+
+(* Distributive lattice theory *)
+Lemma joinIr : right_distributive (@join _ L) (@meet _ L).
+Proof. exact: (@meetUr _ [latticeType of L^r]). 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).
+
+Fact comparableT x y : x >=< y. Proof. exact: le_total. Qed.
+Hint Resolve comparableT.
+
+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 Mixin := LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+
+End TotalLattice.
+End TotalLattice.
+
+Module TotalTheory.
+Section TotalTheory.
+Context {display : unit}.
+Local Notation orderType := (orderType display).
+Context {T : orderType}.
+Implicit Types (x y : T).
+
+Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed.
+Hint Resolve le_total.
+
+Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed.
+Hint Resolve comparableT.
+
+Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s).
+Proof. exact: sort_sorted. Qed.
+
+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.
+
+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.
+
+Lemma leNgt x y : (x <= y) = ~~ (y < x).
+Proof. by rewrite comparable_leNgt. Qed.
+
+Lemma ltNge x y : (x < y) = ~~ (y <= x).
+Proof. by rewrite comparable_ltNge. Qed.
+
+Definition ltgtP := TotalLattice.ltgtP le_total.
+Definition leP := TotalLattice.leP le_total.
+Definition ltP := TotalLattice.ltP le_total.
+
+End TotalTheory.
+End TotalTheory.
+
+
+Module Import BLatticeTheory.
+Section BLatticeTheory.
+Context {disp : unit}.
+Local Notation blatticeType := (blatticeType disp).
+Context {L : blatticeType}.
+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 lex0 x : (x <= 0) = (x == 0).
+Proof. by rewrite le_eqVlt (le_gtF (le0x _)) orbF. Qed.
+
+Lemma ltx0 x : (x < 0) = false.
+Proof. by rewrite lt_neqAle lex0 andNb. Qed.
+
+Lemma lt0x x : (0 < x) = (x != 0).
+Proof. by rewrite lt_neqAle le0x andbT eq_sym. Qed.
+
+Lemma meet0x : left_zero 0 (@meet _ L).
+Proof. by move=> x; apply/eqP; rewrite -leEmeet. Qed.
+
+Lemma meetx0 : right_zero 0 (@meet _ L).
+Proof. by move=> x; rewrite meetC meet0x. Qed.
+
+Lemma join0x : left_id 0 (@join _ L).
+Proof. by move=> x; apply/eqP; rewrite -leEjoin. Qed.
+
+Lemma joinx0 : right_id 0 (@join _ L).
+Proof. by move=> x; rewrite joinC join0x. Qed.
+
+Lemma leU2l_le y t x z : x `&` t = 0 -> x `|` y <= z `|` t -> x <= z.
+Proof.
+by move=> xIt0 /(leI2 (lexx x)); rewrite joinKI meetUr xIt0 joinx0 leIidl.
+Qed.
+
+Lemma leU2r_le y t x z : x `&` t = 0 -> y `|` x <= t `|` z -> x <= z.
+Proof. by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed.
+
+Lemma lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y).
+Proof.
+move=> xz0; apply/idP/idP=> xy; last by rewrite lexU ?xy.
+by apply: (@leU2l_le x z); rewrite ?joinxx.
+Qed.
+
+Lemma lexUr z x y : x `&` z = 0 -> (x <= z `|` y) = (x <= y).
+Proof. by move=> xz0; rewrite joinC; rewrite lexUl. Qed.
+
+Lemma 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.
+by move=> lexyzt; rewrite (leU2l_le _ lexyzt) // (leU2r_le _ lexyzt).
+Qed.
+
+Lemma join_eq0 x y : (x `|` y == 0) = (x == 0) && (y == 0).
+Proof.
+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 :=
+    Eq0NotPOs : x = 0 -> eq0_xor_gt0 x true false
+  | POsNotEq0 : 0 < x -> eq0_xor_gt0 x false true.
+
+Lemma posxP x : eq0_xor_gt0 x (x == 0) (0 < x).
+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) :
+   P j -> F j <= \join_(i | P i) F i.
+Proof. by move=> Pj; rewrite (bigD1 j) //= lexU ?lexx. Qed.
+
+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) :
+   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)).
+  by elim/big_rec2: _ => [|i y b Pi <-]; rewrite ?le0x ?leUx.
+rewrite big_all_cond; apply: (iffP allP) => /= H i;
+have := H i _; rewrite mem_index_enum; last by move/implyP->.
+by move=> /(_ isT) /implyP.
+Qed.
+
+Lemma le_joins (I : finType) (A B : {set I}) (F : I -> L) :
+   A \subset B -> \join_(i in A) F i <= \join_(i in B) F i.
+Proof.
+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.
+Qed.
+
+Lemma joins_setU (I : finType) (A B : {set I}) (F : I -> L) :
+   \join_(i in (A :|: B)) F i = \join_(i in A) F i `|` \join_(i in B) F i.
+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].
+Qed.
+
+Lemma join_seq (I : finType) (r : seq I) (F : I -> L) :
+   \join_(i <- r) F i = \join_(i in r) F i.
+Proof.
+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 //.
+by rewrite join_sup ?orbT ?inE.
+Qed.
+
+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).
+  rewrite big_all_cond; apply/allP => i _ /=.
+  by apply/implyP => /d_Fi_disj ->.
+elim/big_rec2: _ => [|i y]; first by rewrite meetx0.
+case; rewrite (andbF, andbT) // => Pi /(_ isT) dy /eqP dFi.
+by rewrite meetUr dy dFi joinxx.
+Qed.
+
+End BLatticeTheory.
+End BLatticeTheory.
+
+Module Import ReverseTBLattice.
+Section ReverseTBLattice.
+Context {disp : unit}.
+Local Notation tblatticeType := (tblatticeType disp).
+Context {L : tblatticeType}.
+
+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 reverse_tblatticeMixin :=
+   @TBLatticeMixin _ [latticeType of L^r] (bottom : L) (@le0x _ L).
+Canonical reverse_tblatticeType := TBLatticeType L^r reverse_tblatticeMixin.
+
+End ReverseTBLattice.
+End ReverseTBLattice.
+
+Module Import ReverseTBLatticeSyntax.
+Section ReverseTBLatticeSyntax.
+Local Notation "0" := bottom.
+Local Notation "1" := top.
+Local Notation join := (@join (reverse_display _) _).
+Local Notation meet := (@meet (reverse_display _) _).
+
+Notation "\join^r_ ( i <- r | P ) F" :=
+  (\big[join/0]_(i <- r | P%B) F%O) : order_scope.
+Notation "\join^r_ ( i <- r ) F" :=
+  (\big[join/0]_(i <- r) F%O) : order_scope.
+Notation "\join^r_ ( i | P ) F" :=
+  (\big[join/0]_(i | P%B) F%O) : order_scope.
+Notation "\join^r_ i F" :=
+  (\big[join/0]_i F%O) : order_scope.
+Notation "\join^r_ ( i : I | P ) F" :=
+  (\big[join/0]_(i : I | P%B) F%O) (only parsing) : order_scope.
+Notation "\join^r_ ( i : I ) F" :=
+  (\big[join/0]_(i : I) F%O) (only parsing) : order_scope.
+Notation "\join^r_ ( m <= i < n | P ) F" :=
+ (\big[join/0]_(m <= i < n | P%B) F%O) : order_scope.
+Notation "\join^r_ ( m <= i < n ) F" :=
+ (\big[join/0]_(m <= i < n) F%O) : order_scope.
+Notation "\join^r_ ( i < n | P ) F" :=
+ (\big[join/0]_(i < n | P%B) F%O) : order_scope.
+Notation "\join^r_ ( i < n ) F" :=
+ (\big[join/0]_(i < n) F%O) : order_scope.
+Notation "\join^r_ ( i 'in' A | P ) F" :=
+ (\big[join/0]_(i in A | P%B) F%O) : order_scope.
+Notation "\join^r_ ( i 'in' A ) F" :=
+ (\big[join/0]_(i in A) F%O) : order_scope.
+
+Notation "\meet^r_ ( i <- r | P ) F" :=
+  (\big[meet/1]_(i <- r | P%B) F%O) : order_scope.
+Notation "\meet^r_ ( i <- r ) F" :=
+  (\big[meet/1]_(i <- r) F%O) : order_scope.
+Notation "\meet^r_ ( i | P ) F" :=
+  (\big[meet/1]_(i | P%B) F%O) : order_scope.
+Notation "\meet^r_ i F" :=
+  (\big[meet/1]_i F%O) : order_scope.
+Notation "\meet^r_ ( i : I | P ) F" :=
+  (\big[meet/1]_(i : I | P%B) F%O) (only parsing) : order_scope.
+Notation "\meet^r_ ( i : I ) F" :=
+  (\big[meet/1]_(i : I) F%O) (only parsing) : order_scope.
+Notation "\meet^r_ ( m <= i < n | P ) F" :=
+ (\big[meet/1]_(m <= i < n | P%B) F%O) : order_scope.
+Notation "\meet^r_ ( m <= i < n ) F" :=
+ (\big[meet/1]_(m <= i < n) F%O) : order_scope.
+Notation "\meet^r_ ( i < n | P ) F" :=
+ (\big[meet/1]_(i < n | P%B) F%O) : order_scope.
+Notation "\meet^r_ ( i < n ) F" :=
+ (\big[meet/1]_(i < n) F%O) : order_scope.
+Notation "\meet^r_ ( i 'in' A | P ) F" :=
+ (\big[meet/1]_(i in A | P%B) F%O) : order_scope.
+Notation "\meet^r_ ( i 'in' A ) F" :=
+ (\big[meet/1]_(i in A) F%O) : order_scope.
+
+End ReverseTBLatticeSyntax.
+End ReverseTBLatticeSyntax.
+
+Module Import TBLatticeTheory.
+Section TBLatticeTheory.
+Context {disp : unit}.
+Local Notation tblatticeType := (tblatticeType disp).
+Context {L : tblatticeType}.
+Implicit Types (x y : L).
+
+Local Notation "1" := top.
+
+Hint Resolve le0x lex1.
+
+Lemma meetx1 : right_id 1 (@meet _ L).
+Proof. exact: (@joinx0 _ [tblatticeType of L^r]). Qed.
+
+Lemma meet1x : left_id 1 (@meet _ L).
+Proof. exact: (@join0x _ [tblatticeType of L^r]). Qed.
+
+Lemma joinx1 : right_zero 1 (@join _ L).
+Proof. exact: (@meetx0 _ [tblatticeType of L^r]). Qed.
+
+Lemma join1x : left_zero 1 (@join _ L).
+Proof. exact: (@meet0x _ [tblatticeType of L^r]). Qed.
+
+Lemma le1x x : (1 <= x) = (x == 1).
+Proof. exact: (@lex0 _ [tblatticeType of L^r]). 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.
+
+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.
+
+Lemma lexIl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y).
+Proof. rewrite joinC; exact: (@lexUl _ [tblatticeType of L^r]). Qed.
+
+Lemma lexIr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y).
+Proof. rewrite joinC; exact: (@lexUr _ [tblatticeType of L^r]). 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.
+Qed.
+
+Lemma meet_eq1 x y : (x `&` y == 1) = (x == 1) && (y == 1).
+Proof. exact: (@join_eq0 _ [tblatticeType of L^r]). Qed.
+
+Canonical meet_monoid := Monoid.Law (@meetA _ _) meet1x meetx1.
+Canonical meet_comoid := Monoid.ComLaw (@meetC _ _).
+
+Canonical meet_muloid := Monoid.MulLaw (@meet0x _ L) (@meetx0 _ _).
+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) :
+   P j -> \meet_(i | P i) F i <= F j.
+Proof. exact: (@join_sup _ [tblatticeType of L^r]). Qed.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+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.
+
+End TBLatticeTheory.
+End TBLatticeTheory.
+
+Module Import CBLatticeTheory.
+Section CBLatticeTheory.
+Context {disp : unit}.
+Local Notation cblatticeType := (cblatticeType disp).
+Context {L : cblatticeType}.
+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.
+
+Lemma subIK x y : (x `\` y) `&` y = 0.
+Proof. by rewrite meetC subKI. Qed.
+
+Lemma meetIB z x y : (z `&` y) `&` (x `\` y) = 0.
+Proof. by rewrite -meetA subKI meetx0. Qed.
+
+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.
+
+Lemma joinBI y x : (x `\` y) `|` (x `&` y) = x.
+Proof. by rewrite joinC joinIB. Qed.
+
+Lemma joinIBC y x : (y `&` x) `|` (x `\` y) = x.
+Proof. by rewrite meetC joinIB. Qed.
+
+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.
+
+Lemma subxx x : x `\` x = 0.
+Proof. by have := subKI x x; rewrite (meet_idPr _). Qed.
+
+Lemma leBl z x y : x <= y -> x `\` z <= y `\` z.
+Proof.
+rewrite -{1}[x](joinIB z) -{1}[y](joinIB z).
+by rewrite leU2E ?meetIB ?meetBI // => /andP [].
+Qed.
+
+Lemma subKU y x : y `|` (x `\` y) = y `|` x.
+Proof.
+apply/eqP; rewrite eq_le leU2 //= leUx leUl.
+by apply/meet_idPl; have := joinIB y x; rewrite joinIl (join_idPr _).
+Qed.
+
+Lemma subUK y x : (x `\` y) `|` y = x `|` y.
+Proof. by rewrite joinC subKU joinC. Qed.
+
+Lemma leBKU y x : y <= x -> y `|` (x `\` y) = x.
+Proof. by move=> /join_idPl {2}<-; rewrite subKU. Qed.
+
+Lemma leBUK y x : y <= x -> (x `\` y) `|` y = x.
+Proof. by move=> leyx; rewrite joinC leBKU. Qed.
+
+Lemma leBLR x y z : (x `\` y <= z) = (x <= y `|` z).
+Proof.
+apply/idP/idP; first by move=> /join_idPl <-; rewrite joinA subKU joinAC leUr.
+by rewrite -{1}[x](joinIB y) => /(leU2r_le (subIK _ _)).
+Qed.
+
+Lemma subUx x y z : (x `|` y) `\` z = (x `\` z) `|` (y `\` z).
+Proof.
+apply/eqP; rewrite eq_le leUx !leBl ?leUr ?leUl ?andbT //.
+by rewrite leBLR joinA subKU joinAC subKU joinAC -joinA leUr.
+Qed.
+
+Lemma sub_eq0 x y : (x `\` y == 0) = (x <= y).
+Proof. by rewrite -lex0 leBLR joinx0. Qed.
+
+Lemma joinxB x y z : x `|` (y `\` z) = ((x `|` y) `\` z) `|` (x `&` z).
+Proof. by rewrite subUx joinAC joinBI. Qed.
+
+Lemma joinBx x y z : (y `\` z) `|` x = ((y `|` x) `\` z) `|` (z `&` x).
+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.
+Qed.
+
+Lemma leB2 x y z t : x <= z -> t <= y -> x `\` y <= z `\` t.
+Proof. by move=> /(@leBl t) ? /(@leBr x) /le_trans ->. Qed.
+
+Lemma meet_eq0E_sub z x y : x <= z -> (x `&` y == 0) = (x <= z `\` y).
+Proof.
+move=> xz; apply/idP/idP; last by move=> /meet_idPr <-; rewrite -meetA meetBI.
+by move=> /eqP xIy_eq0; rewrite -[x](joinIB y) xIy_eq0 join0x leBl.
+Qed.
+
+Lemma leBRL x y z : (x <= z `\` y) = (x <= z) && (x `&` y == 0).
+Proof.
+apply/idP/idP => [xyz|]; first by rewrite (@meet_eq0E_sub z) // (le_trans xyz).
+by move=> /andP [?]; rewrite -meet_eq0E_sub.
+Qed.
+
+Lemma eq_sub x y z : (x `\` y == z) = (z <= x <= y `|` z) && (z `&` y == 0).
+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.
+by rewrite meet0x meetx0 joinx0.
+Qed.
+
+Lemma subx0 x : x `\` 0 = x.
+Proof. by apply/eqP; rewrite eq_sub join0x meetx0 lexx eqxx. Qed.
+
+Lemma sub0x x : 0 `\` x = 0.
+Proof. by apply/eqP; rewrite eq_sub joinx0 meet0x lexx eqxx le0x. Qed.
+
+Lemma subIx x y z : (x `&` y) `\` z = (x `\` z) `&` (y `\` z).
+Proof.
+apply/eqP; rewrite eq_sub joinIr ?leI2 ?subKU ?leUr ?leBx //=.
+by rewrite -meetA subIK meetx0.
+Qed.
+
+Lemma meetxB x y z : x `&` (y `\` z) = (x `&` y) `\` z.
+Proof. by rewrite subIx -{1}[x](joinBI z) meetUl meetIB joinx0. Qed.
+
+Lemma meetBx x y z : (x `\` y) `&` z = (x `&` z) `\` y.
+Proof. by rewrite ![_ `&` z]meetC meetxB. Qed.
+
+Lemma subxI x y z : x `\` (y `&` z) = (x `\` y) `|` (x `\` z).
+Proof.
+apply/eqP; rewrite eq_sub leUx !leBx //= joinIl joinA joinCA !subKU.
+rewrite joinCA -joinA [_ `|` x]joinC ![x `|` _](join_idPr _) //.
+by rewrite -joinIl leUr /= meetUl {1}[_ `&` z]meetC ?meetBI joinx0.
+Qed.
+
+Lemma subBx x y z : (x `\` y) `\` z = x `\` (y `|` z).
+Proof.
+apply/eqP; rewrite eq_sub leBr ?leUl //=.
+rewrite subxU joinIr subKU -joinIr (meet_idPl _) ?leUr //=.
+by rewrite -meetA subIK meetx0.
+Qed.
+
+Lemma subxB x y z : x `\` (y `\` z) = (x `\` y) `|` (x `&` z).
+Proof.
+rewrite -[y in RHS](joinIB z) subxU joinIl subxI -joinA.
+rewrite joinBI (join_idPl _) // joinBx [x `|` _](join_idPr _) ?leIl //.
+by rewrite meetA meetAC subIK meet0x joinx0 (meet_idPr _).
+Qed.
+
+Lemma joinBK x y : (y `|` x) `\` x = (y `\` x).
+Proof. by rewrite subUx subxx joinx0. Qed.
+
+Lemma joinBKC x y : (x `|` y) `\` x = (y `\` x).
+Proof. by rewrite subUx subxx join0x. Qed.
+
+Lemma disj_le x y : x `&` y == 0 -> x <= y = (x == 0).
+Proof.
+have [->|x_neq0] := altP (x =P 0); first by rewrite le0x.
+by apply: contraTF => lexy; rewrite (meet_idPl _).
+Qed.
+
+Lemma disj_leC x y : y `&` x == 0 -> x <= y = (x == 0).
+Proof. by rewrite meetC => /disj_le. Qed.
+
+Lemma disj_subl x y : x `&` y == 0 -> x `\` y = x.
+Proof. by move=> dxy; apply/eqP; rewrite eq_sub dxy lexx leUr. Qed.
+
+Lemma disj_subr x y : x `&` y == 0 -> y `\` x = y.
+Proof. by rewrite meetC => /disj_subl. Qed.
+
+Lemma lt0B x y : x < y -> 0 < y `\` x.
+Proof.
+by move=> ?; rewrite lt_leAnge leBRL leBLR le0x meet0x eqxx joinx0 /= lt_geF.
+Qed.
+
+End CBLatticeTheory.
+End CBLatticeTheory.
+
+Module Import CTBLatticeTheory.
+Section CTBLatticeTheory.
+Context {disp : unit}.
+Local Notation ctblatticeType := (ctblatticeType disp).
+Context {L : ctblatticeType}.
+Implicit Types (x y z : L).
+Local Notation "0" := bottom.
+Local Notation "1" := top.
+
+Lemma complE x : ~` x = 1 `\` x.
+Proof. by case: L x => [? [? ? []]]. Qed.
+
+Lemma sub1x x : 1 `\` x = ~` x.
+Proof. by rewrite complE. Qed.
+
+Lemma subE x y : x `\` y = x `&` ~` y.
+Proof. by rewrite complE meetxB meetx1. Qed.
+
+Lemma complK : involutive (@compl _ L).
+Proof. by move=> x; rewrite !complE subxB subxx meet1x join0x. Qed.
+
+Lemma compl_inj : injective (@compl _ L).
+Proof. exact/inv_inj/complK. Qed.
+
+Lemma disj_leC x y : (x `&` y == 0) = (x <= ~` y).
+Proof. by rewrite -sub_eq0 subE complK. Qed.
+
+Lemma leC x y : (~` x <= ~` y) = (y <= x).
+Proof.
+gen have leC : x y / y <= x -> ~` x <= ~` y; last first.
+  by apply/idP/idP=> /leC; rewrite ?complK.
+by move=> leyx; rewrite !complE leBr.
+Qed.
+
+Lemma complU x y : ~` (x `|` y) = ~` x `&` ~` y.
+Proof. by rewrite !complE subxU. Qed.
+
+Lemma complI  x y : ~` (x `&` y) = ~` x `|` ~` y.
+Proof. by rewrite !complE subxI. Qed.
+
+Lemma joinxC  x :  x `|` ~` x = 1.
+Proof. by rewrite complE subKU joinx1. Qed.
+
+Lemma joinCx  x : ~` x `|` x = 1.
+Proof. by rewrite joinC joinxC. Qed.
+
+Lemma meetxC  x :  x `&` ~` x = 0.
+Proof. by rewrite complE subKI. Qed.
+
+Lemma meetCx  x : ~` x `&` x = 0.
+Proof. by rewrite meetC meetxC. Qed.
+
+Lemma compl1 : ~` 1 = 0 :> L.
+Proof. by rewrite complE subxx. Qed.
+
+Lemma compl0 : ~` 0 = 1 :> L.
+Proof. by rewrite complE subx0. Qed.
+
+Lemma complB x y : ~` (x `\` y) = ~` x `|` y.
+Proof. by rewrite !complE subxB meet1x. Qed.
+
+Lemma leBC x y : x `\` y <= ~` y.
+Proof. by rewrite leBLR joinxC lex1. Qed.
+
+Lemma leCx x y : (~` x <= y) = (~` y <= x).
+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) :
+   ~` (\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) :
+   ~` (\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.
+
+End CTBLatticeTheory.
+End CTBLatticeTheory.
+
+(*************)
+(* INSTANCES *)
+(*************)
+
+Module Import 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 leEnat (n m : nat): (n <= m) = (n <= m)%N.
+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.
+
+Notation "@max" := (@join nat_display).
+Notation max := (@join nat_display _).
+Notation "@min" := (@meet nat_display).
+Notation min := (@meet nat_display _).
+
+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.
+
+End NatOrder.
+
+
+Module SeqLexPOrder.
+Section SeqLexPOrder.
+Context {display : unit}.
+Local Notation porderType := (porderType display).
+Variable T : porderType.
+
+Implicit Types s : seq T.
+
+Fixpoint lexi s1 s2 :=
+  if s1 is x1 :: s1' then
+    if s2 is x2 :: s2' then
+      (x1 < x2) || ((x1 == x2) && lexi 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.
+Proof. by elim => [|x s ih] //=; rewrite eqxx ih orbT. Qed.
+
+Fact lexi_anti: antisymmetric lexi.
+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.
+Proof.
+elim=> [|y sy ih] [|x sx] [|z sz] //=.
+case: (comparableP x y) => //=; case: (comparableP y z) => //=.
+- by move=> -> -> lesxsy /(ih _ _ lesxsy) ->; rewrite eqxx orbT.
+- by move=> ltyz ->; rewrite ltyz.
+- by move=> -> ->.
+- 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.
+
+End SeqLexPOrder.
+End SeqLexPOrder.
+
+Canonical SeqLexPOrder.lexi_porderType.
+
+Module Def.
+Export POrderDef.
+Export LatticeDef.
+Export BLatticeDef.
+Export TBLatticeDef.
+Export CBLatticeDef.
+Export CTBLatticeDef.
+End Def.
+
+Module Syntax.
+Export POSyntax.
+Export LatticeSyntax.
+Export BLatticeSyntax.
+Export TBLatticeSyntax.
+Export CBLatticeSyntax.
+Export CTBLatticeSyntax.
+Export ReverseSyntax.
+End Syntax.
+
+Module Theory.
+Export ReversePOrder.
+Export POrderTheory.
+Export TotalTheory.
+Export ReverseLattice.
+Export LatticeTheoryMeet.
+Export LatticeTheoryJoin.
+Export BLatticeTheory.
+Export CBLatticeTheory.
+Export ReverseTBLattice.
+Export TBLatticeTheory.
+Export CTBLatticeTheory.
+Export NatOrder.
+Export SeqLexPOrder.
+
+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.
+End Theory.
+
+End Order.