Library mathcomp.ssreflect.order

(* (c) Copyright 2006-2019 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import path fintype tuple bigop finset div prime.

This files defines types equipped with order relations.
Use one of the following modules implementing different theories: Order.LTheory: partially ordered types and lattices excluding complement and totality related theorems. Order.CTheory: complemented lattices including Order.LTheory. Order.TTheory: totally ordered types including Order.LTheory. Order.Theory: ordered types including all of the above theory modules
To access the definitions, notations, and the theory from, say, "Order.Xyz", insert "Import Order.Xyz." at the top of your scripts. Notations are accessible by opening the scope "order_scope" bound to the delimiting key "O".
We provide the following structures of ordered types porderType d == the type of partially ordered types latticeType d == the type of non-distributive lattices bLatticeType d == latticeType with a bottom element tbLatticeType d == latticeType with both a top and a bottom distrLatticeType d == the type of distributive lattices bDistrLatticeType d == distrLatticeType with a bottom element tbDistrLatticeType d == distrLatticeType with both a top and a bottom cbDistrLatticeType d == the type of sectionally complemented distributive lattices (lattices with bottom and a difference operation) ctbDistrLatticeType d == the type of complemented distributive lattices (lattices with top, bottom, difference, and complement) orderType d == the type of totally ordered types finPOrderType d == the type of partially ordered finite types finLatticeType d == the type of nonempty finite non-distributive lattices finDistrLatticeType d == the type of nonempty finite distributive lattices finCDistrLatticeType d == the type of nonempty finite complemented distributive lattices finOrderType d == the type of nonempty totally ordered finite types
Each generic partial order and lattice operations symbols also has a first argument which is the display, the second which is the minimal structure they operate on and then the operands. Here is the exhaustive list of all such symbols for partial orders and lattices together with their default display (as displayed by Check). We document their meaning in the paragraph after the next.
For porderType T @Order.le disp T == <=%O (in fun_scope) @Order.lt disp T == <%O (in fun_scope) @Order.comparable disp T == >=<%O (in fun_scope) @Order.ge disp T == >=%O (in fun_scope) @Order.gt disp T == >%O (in fun_scope) @Order.leif disp T == <?=%O (in fun_scope) For distrLatticeType T @Order.meet disp T x y == x `&` y (in order_scope) @Order.join disp T x y == x `|` y (in order_scope) For bDistrLatticeType T @Order.bottom disp T == 0 (in order_scope) For tbDistrLatticeType T @Order.top disp T == 1 (in order_scope) For cbDistrLatticeType T @Order.sub disp T x y == x `|` y (in order_scope) For ctbDistrLatticeType T @Order.compl disp T x == ~` x (in order_scope)
This first argument named either d, disp or display, of type unit, configures the printing of notations. Instantiating d with tt or an unknown key will lead to a default display for notations, i.e. we have: For x, y of type T, where T is canonically a porderType d: x <= y <-> x is less than or equal to y. x < y <-> x is less than y (:= (y != x) && (x <= y)). min x y <-> if x < y then x else y max x y <-> if x < y then y else x x >= y <-> x is greater than or equal to y (:= y <= x). x > y <-> x is greater than y (:= y < x). x <= y ?= iff C <-> x is less than y, or equal iff C is true. x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)). x >< y <-> x and y are incomparable (:= ~~ x >=< y). For x, y of type T, where T is canonically a distrLatticeType d: x `&` y == the meet of x and y. x `|` y == the join of x and y. In a type T, where T is canonically a bDistrLatticeType d: 0 == the bottom element. \join<range> e == iterated join of a lattice with a bottom. In a type T, where T is canonically a tbDistrLatticeType d: 1 == the top element. \meet<range> e == iterated meet of a lattice with a top. For x, y of type T, where T is canonically a cbDistrLatticeType d: x `\` y == the (sectional) complement of y in [0, x]. For x of type T, where T is canonically a ctbDistrLatticeType d: ~` x == the complement of x in [0, 1].
There are three distinct uses of the symbols <, <=, >, >=, _ <= _ ?= iff _, >=<, and >< in the default display: they can be 0-ary, unary (prefix), and binary (infix). 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable. 1. (< x), (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x). So (< x) is a predicate characterizing elements smaller than x. 2. (x < y), (x <= y), ... mean what they are expected to. These conventions are compatible with Haskell's, where ((< y) x) = (x < y) = ((<) x y), except that we write <%O instead of (<).
Alternative notation displays can be defined by : 1. declaring a new opaque definition of type unit. Using the idiom `Lemma my_display : unit. Proof. exact: tt. Qed.` 2. using this symbol to tag canonical porderType structures using `Canonical my_porderType := POrderType my_display my_type my_mixin`, 3. declaring notations for the main operations of this library, by setting the first argument of the definition to the display, e.g. `Notation my_syndef_le x y := @Order.le my_display _ x y.` or `Notation "x <=< y" := @Order.lt my_display _ x y (at level ...).` Non overloaded notations will default to the default display.
One may use displays either for convenience or to disambiguate between different structures defined on "copies" of a type (as explained below.) We provide the following "copies" of types, the first one is a *documented example* natdvd := nat == a "copy" of nat which is canonically ordered using divisibility predicate dvdn. Notation %|, %<|, gcd, lcm are used instead of <=, <, meet and join. T^d := dual T, where dual is a new definition for (fun T => T) == a "copy" of T, such that if T is canonically ordered, then T^d is canonically ordered with the dual order, and displayed with an extra ^d in the notation i.e. <=^d, <^d, >=<^d, ><^d, `&`^d, `|`^d are used and displayed instead of <=, <, >=<, ><, `&`, `|` T *prod[d] T' := T * T' == a "copy" of the cartesian product such that, if T and T' are canonically ordered, then T *prod[d] T' is canonically ordered in product order. i.e. (x1, x2) <= (y1, y2) = (x1 <= y1) && (x2 <= y2), and displayed in display d T *p T' := T *prod[prod_display] T' where prod_display adds an extra ^p to all notations T *lexi[d] T' := T * T' == a "copy" of the cartesian product such that, if T and T' are canonically ordered, then T *lexi[d] T' is canonically ordered in lexicographic order i.e. (x1, x2) <= (y1, y2) = (x1 <= y1) && ((x1 >= y1) ==> (x2 <= y2)) and (x1, x2) < (y1, y2) = (x1 <= y1) && ((x1 >= y1) ==> (x2 < y2)) and displayed in display d T *l T' := T *lexi[lexi_display] T' where lexi_display adds an extra ^l to all notations seqprod_with d T := seq T == a "copy" of seq, such that if T is canonically ordered, then seqprod_with d T is canonically ordered in product order i.e. [:: x1, .., xn] <= [y1, .., yn] = (x1 <= y1) && ... && (xn <= yn) and displayed in display d n.-tupleprod[d] T == same with n.tuple T seqprod T := seqprod_with prod_display T n.-tupleprod T := n.-tuple[prod_display] T seqlexi_with d T := seq T == a "copy" of seq, such that if T is canonically ordered, then seqprod_with d T is canonically ordered in lexicographic order i.e. [:: x1, .., xn] <= [y1, .., yn] = (x1 <= x2) && ((x1 >= y1) ==> ((x2 <= y2) && ...)) and displayed in display d n.-tuplelexi[d] T == same with n.tuple T seqlexi T := lexiprod_with lexi_display T n.-tuplelexi T := n.-tuple[lexi_display] T
Beware that canonical structure inference will not try to find the copy of the structures that fits the display one mentioned, but will rather determine which canonical structure and display to use depending on the copy of the type one provided. In this sense they are merely displays to inform the user of what the inference did, rather than additional input for the inference.
Existing displays are either dual_display d (where d is a display), dvd_display (both explained above), ring_display (from algebra/ssrnum to change the scope of the usual notations to ring_scope). We also provide lexi_display and prod_display for lexicographic and product order respectively. The default display is tt and users can define their own as explained above.
For porderType we provide the following operations [arg min(i < i0 | P) M] == a value i : T minimizing M : R, subject to the condition P (i may appear in P and M), and provided P holds for i0. [arg max(i > i0 | P) M] == a value i maximizing M subject to P and provided P holds for i0. [arg min(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. [arg max(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. [arg min(i < i0) M] == an i : T minimizing M, given i0 : T. [arg max(i > i0) M] == an i : T maximizing M, given i0 : T. with head symbols Order.arg_min and Order.arg_max The user may use extremumP or extremum_inP to eliminate them.
In order to build the above structures, one must provide the appropriate mixin to the following structure constructors. The list of possible mixins is indicated after each constructor. Each mixin is documented in the next paragraph.
POrderType disp T pord_mixin == builds a porderType from a canonical choiceType instance of T where pord_mixin can be of types lePOrderMixin, ltPOrderMixin, meetJoinMixin, leOrderMixin, or ltOrderMixin or computed using PcanPOrderMixin or CanPOrderMixin. disp is a display as explained above
LatticeType T lat_mixin == builds a latticeType from a porderType where lat_mixin can be of types latticeMixin, meetJoinMixin, leOrderMixin, ltOrderMixin, totalPOrderMixin or computed using IsoLatticeMixin.
DistrLatticeType T lat_mixin == builds a distrLatticeType from a porderType where lat_mixin can be of types distrLatticeMixin, meetJoinMixin, leOrderMixin leOrderMixin, ltOrderMixin, totalPOrderMixin, or totalLatticeMixin or computed using IsoLatticeMixin.
BLatticeType T bot_mixin == builds a bDistrLatticeType from a distrLatticeType and a bottom element
TBLatticeType T top_mixin == builds a tbDistrLatticeType from a bDistrLatticeType and a top element
CBLatticeType T sub_mixin == builds a cbDistrLatticeType from a bDistrLatticeType and a difference operation
CTBLatticeType T compl_mixin == builds a ctbDistrLatticeType from a tbDistrLatticeType and a complement operation
OrderType T ord_mixin == builds an orderType from a distrLatticeType where ord_mixin can be of types leOrderMixin, ltOrderMixin, totalPOrderMixin, totalLatticeMixin, or totalOrderMixin or computed using MonoTotalMixin.
Additionally:
  • [porderType of _ ] ... notations are available to recover structures on "copies" of the types, as in eqtype, choicetype, ssralg...
  • [finPOrderType of _ ] ... notations to compute joins between finite types and ordered types
List of possible mixins (a.k.a. factories):
  • lePOrderMixin == on a choiceType, takes le, lt, reflexivity, antisymmetry and transitivity of le. (can build: porderType)
  • ltPOrderMixin == on a choiceType, takes le, lt, irreflexivity and transitivity of lt. (can build: porderType)
  • meetJoinMixin == on a choiceType, takes le, lt, meet, join, commutativity and associativity of meet and join idempotence of meet and some De Morgan laws (can build: porderType, latticeType, distrLatticeType)
  • leOrderMixin == on a choiceType, takes le, lt, meet, join antisymmetry, transitivity and totality of le. (can build: porderType, latticeType, distrLatticeType, orderType)
  • ltOrderMixin == on a choiceType, takes le, lt, irreflexivity, transitivity and totality of lt. (can build: porderType, latticeType, distrLatticeType, orderType)
  • totalPOrderMixin == on a porderType T, totality of the order of T := total (<=%O : rel T) (can build: latticeType, distrLatticeType, orderType)
  • totalLatticeMixin == on a latticeType T, totality of the order of T := total (<=%O : rel T) (can build distrLatticeType, orderType)
  • totalOrderMixin == on a distrLatticeType T, totality of the order of T := total (<=%O : rel T) (can build: orderType) NB: the above three mixins are kept separate from each other (even though they are convertible), in order to avoid ambiguous coercion paths.
  • distrLatticeMixin == on a latticeType T, takes meet, join commutativity and associativity of meet and join idempotence of meet and some De Morgan laws (can build: distrLatticeType)
  • bDistrLatticeMixin, tbDistrLatticeMixin, cbDistrLatticeMixin, ctbDistrLatticeMixin == mixins with one extra operation (respectively bottom, top, relative complement, and total complement)
Additionally:
  • [porderMixin of T by <: ] creates a porderMixin by subtyping.
  • [totalOrderMixin of T by <: ] creates the associated totalOrderMixin.
  • PCanPOrderMixin, CanPOrderMixin create porderMixin from cancellations
  • MonoTotalMixin creates a totalPOrderMixin from monotonicity
  • IsoLatticeMixin creates a distrLatticeMixin from an ordered structure isomorphism (i.e., cancel f f', cancel f' f, {mono f : x y / x <= y})
List of "big pack" notations:
  • DistrLatticeOfChoiceType builds a distrLatticeType from a choiceType and a meetJoinMixin.
  • OrderOfChoiceType builds an orderType from a choiceType, and a leOrderMixin or a ltOrderMixin.
  • OrderOfPOrder builds an orderType from a porderType and a totalPOrderMixin.
  • OrderOfLattice builds an orderType from a latticeType and a totalLatticeMixin.
NB: These big pack notations should be used only to construct instances on the fly, e.g., in the middle of a proof, and should not be used to declare canonical instances. See field/algebraics_fundamentals.v for an example usage.
We provide the following canonical instances of ordered types
  • all possible structures on bool
  • porderType, latticeType, distrLatticeType, orderType and bDistrLatticeType on nat for the leq order
  • porderType, latticeType, distrLatticeType, bDistrLatticeType, cbDistrLatticeType, ctbDistrLatticeType on nat for the dvdn order, where meet and join are respectively gcdn and lcmn
  • porderType, latticeType, distrLatticeType, orderType, bDistrLatticeType, tbDistrLatticeType, cbDistrLatticeType, ctbDistrLatticeType on T *prod[disp] T' a "copy" of T * T' using product order (and T *p T' its specialization to prod_display)
  • porderType, latticeType, distrLatticeType, and orderType, on T *lexi[disp] T' another "copy" of T * T', with lexicographic ordering (and T *l T' its specialization to lexi_display)
  • porderType, latticeType, distrLatticeType, and orderType, on {t : T & T' x} with lexicographic ordering
  • porderType, latticeType, distrLatticeType, orderType, bDistrLatticeType, cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType on seqprod_with disp T a "copy" of seq T using product order (and seqprod T' its specialization to prod_display)
  • porderType, latticeType, distrLatticeType, and orderType, on seqlexi_with disp T another "copy" of seq T, with lexicographic ordering (and seqlexi T its specialization to lexi_display)
  • porderType, latticeType, distrLatticeType, orderType, bDistrLatticeType, cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType on n.-tupleprod[disp] a "copy" of n.-tuple T using product order (and n.-tupleprod T its specialization to prod_display)
  • porderType, latticeType, distrLatticeType, and orderType, on n.-tuplelexi[d] T another "copy" of n.-tuple T, with lexicographic ordering (and n.-tuplelexi T its specialization to lexi_display)
and all possible finite type instances
In order to get a canonical order on prod or seq, one may import modules DefaultProdOrder or DefaultProdLexiOrder, DefaultSeqProdOrder or DefaultSeqLexiOrder, and DefaultTupleProdOrder or DefaultTupleLexiOrder.
On orderType, leP ltP ltgtP are the three main lemmas for case analysis. On porderType, one may use comparableP, comparable_leP, comparable_ltP, and comparable_ltgtP, which are the four main lemmas for case analysis.
We also provide specialized versions of some theorems from path.v.
This file is based on prior work by D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani

Set Implicit Arguments.

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 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).

Notations for dual partial and total order
Reserved Notation "x <=^d y" (at level 70, y at next level).
Reserved Notation "x >=^d y" (at level 70, y at next level).
Reserved Notation "x <^d y" (at level 70, y at next level).
Reserved Notation "x >^d y" (at level 70, y at next level).
Reserved Notation "x <=^d y :> T" (at level 70, y at next level).
Reserved Notation "x >=^d y :> T" (at level 70, y at next level).
Reserved Notation "x <^d y :> T" (at level 70, y at next level).
Reserved Notation "x >^d y :> T" (at level 70, y at next level).
Reserved Notation "<=^d y" (at level 35).
Reserved Notation ">=^d y" (at level 35).
Reserved Notation "<^d y" (at level 35).
Reserved Notation ">^d y" (at level 35).
Reserved Notation "<=^d y :> T" (at level 35, y at next level).
Reserved Notation ">=^d y :> T" (at level 35, y at next level).
Reserved Notation "<^d y :> T" (at level 35, y at next level).
Reserved Notation ">^d y :> T" (at level 35, y at next level).
Reserved Notation "x >=<^d y" (at level 70, no associativity).
Reserved Notation ">=<^d x" (at level 35).
Reserved Notation ">=<^d y :> T" (at level 35, y at next level).
Reserved Notation "x ><^d y" (at level 70, no associativity).
Reserved Notation "><^d x" (at level 35).
Reserved Notation "><^d y :> T" (at level 35, y at next level).

Reserved Notation "x <=^d y <=^d z" (at level 70, y, z at next level).
Reserved Notation "x <^d y <=^d z" (at level 70, y, z at next level).
Reserved Notation "x <=^d y <^d z" (at level 70, y, z at next level).
Reserved Notation "x <^d y <^d z" (at level 70, y, z at next level).
Reserved Notation "x <=^d y ?= 'iff' c" (at level 70, y, c at next level,
  format "x '[hv' <=^d y '/' ?= 'iff' c ']'").
Reserved Notation "x <=^d y ?= 'iff' c :> T" (at level 70, y, c at next level,
  format "x '[hv' <=^d y '/' ?= 'iff' c :> T ']'").

Reserved notation for dual lattice operations.
Reserved Notation "A `&^d` B" (at level 48, left associativity).
Reserved Notation "A `|^d` B" (at level 52, left associativity).
Reserved Notation "A `\^d` B" (at level 50, left associativity).
Reserved Notation "~^d` A" (at level 35, right associativity).

Reserved notations for product ordering of prod or seq
Reserved Notation "x <=^p y" (at level 70, y at next level).
Reserved Notation "x >=^p y" (at level 70, y at next level).
Reserved Notation "x <^p y" (at level 70, y at next level).
Reserved Notation "x >^p y" (at level 70, y at next level).
Reserved Notation "x <=^p y :> T" (at level 70, y at next level).
Reserved Notation "x >=^p y :> T" (at level 70, y at next level).
Reserved Notation "x <^p y :> T" (at level 70, y at next level).
Reserved Notation "x >^p y :> T" (at level 70, y at next level).
Reserved Notation "<=^p y" (at level 35).
Reserved Notation ">=^p y" (at level 35).
Reserved Notation "<^p y" (at level 35).
Reserved Notation ">^p y" (at level 35).
Reserved Notation "<=^p y :> T" (at level 35, y at next level).
Reserved Notation ">=^p y :> T" (at level 35, y at next level).
Reserved Notation "<^p y :> T" (at level 35, y at next level).
Reserved Notation ">^p y :> T" (at level 35, y at next level).
Reserved Notation "x >=<^p y" (at level 70, no associativity).
Reserved Notation ">=<^p x" (at level 35).
Reserved Notation ">=<^p y :> T" (at level 35, y at next level).
Reserved Notation "x ><^p y" (at level 70, no associativity).
Reserved Notation "><^p x" (at level 35).
Reserved Notation "><^p y :> T" (at level 35, y at next level).

Reserved Notation "x <=^p y <=^p z" (at level 70, y, z at next level).
Reserved Notation "x <^p y <=^p z" (at level 70, y, z at next level).
Reserved Notation "x <=^p y <^p z" (at level 70, y, z at next level).
Reserved Notation "x <^p y <^p z" (at level 70, y, z at next level).
Reserved Notation "x <=^p y ?= 'iff' c" (at level 70, y, c at next level,
  format "x '[hv' <=^p y '/' ?= 'iff' c ']'").
Reserved Notation "x <=^p y ?= 'iff' c :> T" (at level 70, y, c at next level,
  format "x '[hv' <=^p y '/' ?= 'iff' c :> T ']'").

Reserved notation for dual lattice operations.
Reserved Notation "A `&^p` B" (at level 48, left associativity).
Reserved Notation "A `|^p` B" (at level 52, left associativity).
Reserved Notation "A `\^p` B" (at level 50, left associativity).
Reserved Notation "~^p` A" (at level 35, right associativity).

Reserved notations for lexicographic ordering of prod or seq
Reserved Notation "x <=^l y" (at level 70, y at next level).
Reserved Notation "x >=^l y" (at level 70, y at next level).
Reserved Notation "x <^l y" (at level 70, y at next level).
Reserved Notation "x >^l y" (at level 70, y at next level).
Reserved Notation "x <=^l y :> T" (at level 70, y at next level).
Reserved Notation "x >=^l y :> T" (at level 70, y at next level).
Reserved Notation "x <^l y :> T" (at level 70, y at next level).
Reserved Notation "x >^l y :> T" (at level 70, y at next level).
Reserved Notation "<=^l y" (at level 35).
Reserved Notation ">=^l y" (at level 35).
Reserved Notation "<^l y" (at level 35).
Reserved Notation ">^l y" (at level 35).
Reserved Notation "<=^l y :> T" (at level 35, y at next level).
Reserved Notation ">=^l y :> T" (at level 35, y at next level).
Reserved Notation "<^l y :> T" (at level 35, y at next level).
Reserved Notation ">^l y :> T" (at level 35, y at next level).
Reserved Notation "x >=<^l y" (at level 70, no associativity).
Reserved Notation ">=<^l x" (at level 35).
Reserved Notation ">=<^l y :> T" (at level 35, y at next level).
Reserved Notation "x ><^l y" (at level 70, no associativity).
Reserved Notation "><^l x" (at level 35).
Reserved Notation "><^l y :> T" (at level 35, y at next level).

Reserved Notation "x <=^l y <=^l z" (at level 70, y, z at next level).
Reserved Notation "x <^l y <=^l z" (at level 70, y, z at next level).
Reserved Notation "x <=^l y <^l z" (at level 70, y, z at next level).
Reserved Notation "x <^l y <^l z" (at level 70, y, z at next level).
Reserved Notation "x <=^l y ?= 'iff' c" (at level 70, y, c at next level,
  format "x '[hv' <=^l y '/' ?= 'iff' c ']'").
Reserved Notation "x <=^l y ?= 'iff' c :> T" (at level 70, y, c at next level,
  format "x '[hv' <=^l y '/' ?= 'iff' c :> T ']'").

Reserved notations for divisibility
Reserved Notation "x %<| y" (at level 70, no associativity).

Reserved Notation "\gcd_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \gcd_ i '/ ' F ']'").
Reserved Notation "\gcd_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \gcd_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \gcd_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\gcd_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \gcd_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \gcd_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \gcd_ ( i | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\gcd_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\gcd_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \gcd_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \gcd_ ( i < n ) F ']'").
Reserved Notation "\gcd_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \gcd_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \gcd_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\lcm_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \lcm_ i '/ ' F ']'").
Reserved Notation "\lcm_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \lcm_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \lcm_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\lcm_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \lcm_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \lcm_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \lcm_ ( i | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\lcm_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\lcm_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \lcm_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \lcm_ ( i < n ) F ']'").
Reserved Notation "\lcm_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \lcm_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \lcm_ ( i 'in' A ) '/ ' F ']'").

Reserved notation for dual lattice operations.
Reserved Notation "A `&^l` B" (at level 48, left associativity).
Reserved Notation "A `|^l` B" (at level 52, left associativity).
Reserved Notation "A `\^l` B" (at level 50, left associativity).
Reserved Notation "~^l` 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).
Reserved Notation "\meet_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
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).
Reserved Notation "\join_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
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 "\min_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \min_ i '/ ' F ']'").
Reserved Notation "\min_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \min_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \min_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \min_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \min_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \min_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\min_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\min_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \min_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \min_ ( i < n ) F ']'").
Reserved Notation "\min_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \min_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \min_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\max_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \max_ i '/ ' F ']'").
Reserved Notation "\max_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \max_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \max_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \max_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \max_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \max_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\max_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\max_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \max_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \max_ ( i < n ) F ']'").
Reserved Notation "\max_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \max_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \max_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^d_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \meet^d_ i '/ ' F ']'").
Reserved Notation "\meet^d_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \meet^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \meet^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \meet^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \meet^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \meet^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\meet^d_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\meet^d_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \meet^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \meet^d_ ( i < n ) F ']'").
Reserved Notation "\meet^d_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \meet^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \meet^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^d_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \join^d_ i '/ ' F ']'").
Reserved Notation "\join^d_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \join^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \join^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^d_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \join^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \join^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \join^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\join^d_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\join^d_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \join^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \join^d_ ( i < n ) F ']'").
Reserved Notation "\join^d_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \join^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \join^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\min^d_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \min^d_ i '/ ' F ']'").
Reserved Notation "\min^d_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \min^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \min^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min^d_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \min^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \min^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \min^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\min^d_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\min^d_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \min^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \min^d_ ( i < n ) F ']'").
Reserved Notation "\min^d_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \min^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \min^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\max^d_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \max^d_ i '/ ' F ']'").
Reserved Notation "\max^d_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \max^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \max^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max^d_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \max^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \max^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \max^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\max^d_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\max^d_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \max^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \max^d_ ( i < n ) F ']'").
Reserved Notation "\max^d_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \max^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \max^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^p_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \meet^p_ i '/ ' F ']'").
Reserved Notation "\meet^p_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \meet^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \meet^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \meet^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \meet^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \meet^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\meet^p_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\meet^p_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \meet^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \meet^p_ ( i < n ) F ']'").
Reserved Notation "\meet^p_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \meet^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \meet^p_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^p_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \join^p_ i '/ ' F ']'").
Reserved Notation "\join^p_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \join^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \join^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^p_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \join^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \join^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \join^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\join^p_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50).
Reserved Notation "\join^p_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \join^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \join^p_ ( i < n ) F ']'").
Reserved Notation "\join^p_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \join^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \join^p_ ( i 'in' A ) '/ ' F ']'").

Module Order.

STRUCTURES

Module POrder.
Section ClassDef.
Record mixin_of (T : eqType) := Mixin {
  le : rel T;
  lt : rel T;
  _ : x y, lt x y = (y != x) && (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)
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack :=
  fun bT b & phant_id (Choice.class bT) b
  fun mPack disp (@Class T b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Canonical eqType.
Canonical choiceType.
Notation porderType := type.
Notation lePOrderMixin := mixin_of.
Notation LePOrderMixin := Mixin.
Notation POrderType disp T m := (@pack T disp _ _ id m).
Notation "[ 'porderType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'porderType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'porderType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0, format "[ 'porderType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'porderType' 'of' T ]" := [porderType of T for _]
  (at level 0, format "[ 'porderType' 'of' T ]") : form_scope.
Notation "[ 'porderType' 'of' T 'with' disp ]" :=
  [porderType of T for _ with disp]
  (at level 0, format "[ 'porderType' 'of' T 'with' disp ]") : form_scope.
End Exports.

End POrder.
Import POrder.Exports.

Section POrderDef.

Variable (disp : unit).
Variable (T : porderType).

Definition le : rel T := POrder.le (POrder.class T).

Definition lt : rel T := POrder.lt (POrder.class T).

Definition comparable : rel T := fun (x y : T) ⇒ (x y) || (y x).

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.

Variant le_xor_gt (x y : T) :
  T T T T bool bool Set :=
  | LeNotGt of x y : le_xor_gt x y x x y y true false
  | GtNotLe of y < x : le_xor_gt x y y y x x false true.

Variant lt_xor_ge (x y : T) :
  T T T T bool bool Set :=
  | LtNotGe of x < y : lt_xor_ge x y x x y y false true
  | GeNotLt of y x : lt_xor_ge x y y y x x true false.

Definition min x y := if x < y then x else y.
Definition max x y := if x < y then y else x.

Variant compare (x y : T) :
   T T T T
   bool bool bool bool bool bool Set :=
  | CompareLt of x < y : compare x y
    x x y y false false false true false true
  | CompareGt of y < x : compare x y
    y y x x false false true false true false
  | CompareEq of x = y : compare x y
    x x x x true true true true false false.

Variant incompare (x y : T) :
   T T T T
  bool bool bool bool bool bool bool bool Set :=
  | InCompareLt of x < y : incompare x y
    x x y y false false false true false true true true
  | InCompareGt of y < x : incompare x y
    y y x x false false true false true false true true
  | InCompare of x >< y : incompare x y
    x y y x false false false false false false false false
  | InCompareEq of x = y : incompare x y
    x x x x true true true true false false true true.

Definition arg_min {I : finType} := @extremum T I le.
Definition arg_max {I : finType} := @extremum T I ge.

End POrderDef.


Module Import POSyntax.

Notation "<=%O" := le : fun_scope.
Notation ">=%O" := ge : fun_scope.
Notation "<%O" := lt : fun_scope.
Notation ">%O" := gt : fun_scope.
Notation "<?=%O" := leif : fun_scope.
Notation ">=<%O" := comparable : fun_scope.
Notation "><%O" := (fun x y~~ (comparable x y)) : fun_scope.

Notation "<= y" := (ge y) : order_scope.
Notation "<= y :> T" := ( (y : T)) (only parsing) : order_scope.
Notation ">= y" := (le y) : order_scope.
Notation ">= y :> T" := ( (y : T)) (only parsing) : order_scope.

Notation "< y" := (gt y) : order_scope.
Notation "< y :> T" := (< (y : T)) (only parsing) : order_scope.
Notation "> y" := (lt y) : order_scope.
Notation "> y :> T" := (> (y : T)) (only parsing) : order_scope.

Notation ">=< y" := (comparable y) : order_scope.
Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope.

Notation "x <= y" := (le x y) : order_scope.
Notation "x <= y :> T" := ((x : T) (y : T)) (only parsing) : 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)) (only parsing) : 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 :> T" := ((x : T) (y : T) ?= 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.

Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
    (arg_min i0 (fun iP%B) (fun iF))
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope.

Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
    [arg min_(i < i0 | i \in A) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope.

Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope.

Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
     (arg_max i0 (fun iP%B) (fun iF))
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope.

Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
    [arg max_(i > i0 | i \in A) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope.

Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope.

End POSyntax.

Module POCoercions.
Coercion le_of_leif : leif >-> is_true.
End POCoercions.

Module Lattice.
Section ClassDef.

Record mixin_of d (T : porderType d) := Mixin {
  meet : T T T;
  join : T T T;
  _ : commutative meet;
  _ : commutative join;
  _ : associative meet;
  _ : associative join;
  _ : y x, meet x (join x y) = x;
  _ : y x, join x (meet x y) = x;
  _ : x y, (x y) = (meet x y == x);
}.

Record class_of (T : Type) := Class {
  base : POrder.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (POrder.Pack mixin_disp base)
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : porderType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@POrder.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> POrder.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion porderType : type >-> POrder.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Notation latticeType := type.
Notation latticeMixin := mixin_of.
Notation LatticeMixin := Mixin.
Notation LatticeType T m := (@pack T _ _ _ m _ _ id _ id).
Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'latticeType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'latticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0, format "[ 'latticeType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'latticeType' 'of' T ]" := [latticeType of T for _]
  (at level 0, format "[ 'latticeType' 'of' T ]") : form_scope.
Notation "[ 'latticeType' 'of' T 'with' disp ]" :=
  [latticeType of T for _ with disp]
  (at level 0, format "[ 'latticeType' 'of' T 'with' disp ]") : form_scope.
End Exports.
End Lattice.
Export Lattice.Exports.

Section LatticeDef.
Context {disp : unit}.
Context {T : latticeType}.
Definition meet : T T T := Lattice.meet (Lattice.class T).
Definition join : T T T := Lattice.join (Lattice.class T).

Variant lel_xor_gt (x y : T) :
  T T T T T T T T bool bool Set :=
  | LelNotGt of x y : lel_xor_gt x y x x y y x x y y true false
  | GtlNotLe of y < x : lel_xor_gt x y y y x x y y x x false true.

Variant ltl_xor_ge (x y : T) :
  T T T T T T T T bool bool Set :=
  | LtlNotGe of x < y : ltl_xor_ge x y x x y y x x y y false true
  | GelNotLt of y x : ltl_xor_ge x y y y x x y y x x true false.

Variant comparel (x y : T) :
   T T T T T T T T
   bool bool bool bool bool bool Set :=
  | ComparelLt of x < y : comparel x y
    x x y y x x y y false false false true false true
  | ComparelGt of y < x : comparel x y
    y y x x y y x x false false true false true false
  | ComparelEq of x = y : comparel x y
    x x x x x x x x true true true true false false.

Variant incomparel (x y : T) :
  T T T T T T T T
  bool bool bool bool bool bool bool bool Set :=
  | InComparelLt of x < y : incomparel x y
    x x y y x x y y false false false true false true true true
  | InComparelGt of y < x : incomparel x y
    y y x x y y x x false false true false true false true true
  | InComparel of x >< y : incomparel x y
    x y y x (meet y x) (meet x y) (join y x) (join x y)
    false false false false false false false false
  | InComparelEq of x = y : incomparel x y
    x x x x x x x x true true true true false false true true.

End LatticeDef.

Module Import LatticeSyntax.

Notation "x `&` y" := (meet x y) : order_scope.
Notation "x `|` y" := (join x y) : order_scope.

End LatticeSyntax.

Module BLattice.
Section ClassDef.
Record mixin_of d (T : porderType d) := Mixin {
  bottom : T;
  _ : x, bottom x;
}.

Record class_of (T : Type) := Class {
  base : Lattice.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (POrder.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : latticeType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@Lattice.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 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 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 _ id)
  (at level 0, format "[ 'bLatticeType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'bLatticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0,
   format "[ 'bLatticeType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'bLatticeType' 'of' T ]" := [bLatticeType of T for _]
  (at level 0, format "[ 'bLatticeType' 'of' T ]") : form_scope.
Notation "[ 'bLatticeType' 'of' T 'with' disp ]" :=
  [bLatticeType of T for _ with disp]
  (at level 0, format "[ 'bLatticeType' 'of' T 'with' disp ]") :
  form_scope.
End Exports.

End BLattice.
Export BLattice.Exports.

Definition bottom {disp : unit} {T : bLatticeType disp} : T :=
  BLattice.bottom (BLattice.class T).

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.
Record mixin_of d (T : porderType d) := Mixin {
  top : T;
  _ : x, x top;
}.

Record class_of (T : Type) := Class {
  base : BLattice.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (POrder.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : bLatticeType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@BLattice.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 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 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 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 _ id)
  (at level 0, format "[ 'tbLatticeType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'tbLatticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0,
   format "[ 'tbLatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope.
Notation "[ 'tbLatticeType' 'of' T ]" := [tbLatticeType of T for _]
  (at level 0, format "[ 'tbLatticeType' 'of' T ]") : form_scope.
Notation "[ 'tbLatticeType' 'of' T 'with' disp ]" :=
  [tbLatticeType of T for _ with disp]
  (at level 0, format "[ 'tbLatticeType' 'of' T 'with' disp ]") : form_scope.
End Exports.

End TBLattice.
Export TBLattice.Exports.

Definition top disp {T : tbLatticeType disp} : T :=
  TBLattice.top (TBLattice.class T).

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 DistrLattice.
Section ClassDef.

Record mixin_of d (T : latticeType d) := Mixin {
  _ : @left_distributive T T meet join;
}.

Record class_of (T : Type) := Class {
  base : Lattice.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (Lattice.Pack mixin_disp base)
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : latticeType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@Lattice.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 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 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 distrLatticeType := type.
Notation distrLatticeMixin := mixin_of.
Notation DistrLatticeMixin := Mixin.
Notation DistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id).
Notation "[ 'distrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'distrLatticeType' 'of' T 'for' cT ]") :
  form_scope.
Notation "[ 'distrLatticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0,
   format "[ 'distrLatticeType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'distrLatticeType' 'of' T ]" := [distrLatticeType of T for _]
  (at level 0, format "[ 'distrLatticeType' 'of' T ]") : form_scope.
Notation "[ 'distrLatticeType' 'of' T 'with' disp ]" :=
  [latticeType of T for _ with disp]
  (at level 0, format "[ 'distrLatticeType' 'of' T 'with' disp ]") :
  form_scope.
End Exports.

End DistrLattice.
Export DistrLattice.Exports.

Module BDistrLattice.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : DistrLattice.class_of T;
  mixin_disp : unit;
  mixin : BLattice.mixin_of (Lattice.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@DistrLattice.class disp bT) b
  fun mT m & phant_id (@BLattice.class disp mT) (BLattice.Class m) ⇒
  Pack disp (@Class T b disp m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition nb_distrLatticeType := @DistrLattice.Pack disp bLatticeType xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> DistrLattice.class_of.
Coercion base2 : class_of >-> BLattice.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.
Coercion bLatticeType : type >-> BLattice.type.
Coercion distrLatticeType : type >-> DistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical distrLatticeType.
Canonical nb_distrLatticeType.
Notation bDistrLatticeType := type.
Notation "[ 'bDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'bDistrLatticeType' 'of' T ]") : form_scope.
End Exports.

End BDistrLattice.
Export BDistrLattice.Exports.

Module TBDistrLattice.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : BDistrLattice.class_of T;
  mixin_disp : unit;
  mixin : TBLattice.mixin_of (BLattice.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@BDistrLattice.class disp bT) b
  fun mT m & phant_id (@TBLattice.class disp mT) (TBLattice.Class m) ⇒
  Pack disp (@Class T b disp m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
Definition ntb_distrLatticeType := @DistrLattice.Pack disp tbLatticeType xclass.
Definition ntb_bDistrLatticeType :=
  @BDistrLattice.Pack disp tbLatticeType xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> BDistrLattice.class_of.
Coercion base2 : class_of >-> TBLattice.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.
Coercion bLatticeType : type >-> BLattice.type.
Coercion tbLatticeType : type >-> TBLattice.type.
Coercion distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Canonical ntb_distrLatticeType.
Canonical ntb_bDistrLatticeType.
Notation tbDistrLatticeType := type.
Notation "[ 'tbDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'tbDistrLatticeType' 'of' T ]") : form_scope.
End Exports.

End TBDistrLattice.
Export TBDistrLattice.Exports.

Module CBDistrLattice.
Section ClassDef.
Record mixin_of d (T : bDistrLatticeType d) := Mixin {
  sub : T T T;
  _ : x y, y `&` sub x y = bottom;
  _ : x y, (x `&` y) `|` sub x y = x
}.

Record class_of (T : Type) := Class {
  base : BDistrLattice.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (BDistrLattice.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : bDistrLatticeType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@BDistrLattice.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 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.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> BDistrLattice.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.
Coercion distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Notation cbDistrLatticeType := type.
Notation cbDistrLatticeMixin := mixin_of.
Notation CBDistrLatticeMixin := Mixin.
Notation CBDistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id).
Notation "[ 'cbDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'cbDistrLatticeType' 'of' T 'for' cT ]") :
  form_scope.
Notation "[ 'cbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0,
   format "[ 'cbDistrLatticeType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'cbDistrLatticeType' 'of' T ]" := [cbDistrLatticeType of T for _]
  (at level 0, format "[ 'cbDistrLatticeType' 'of' T ]") : form_scope.
Notation "[ 'cbDistrLatticeType' 'of' T 'with' disp ]" :=
  [cbDistrLatticeType of T for _ with disp]
  (at level 0, format "[ 'cbDistrLatticeType' 'of' T 'with' disp ]") :
  form_scope.
End Exports.

End CBDistrLattice.
Export CBDistrLattice.Exports.

Definition sub {disp : unit} {T : cbDistrLatticeType disp} : T T T :=
  CBDistrLattice.sub (CBDistrLattice.class T).

Module Import CBDistrLatticeSyntax.
Notation "x `\` y" := (sub x y) : order_scope.
End CBDistrLatticeSyntax.

Module CTBDistrLattice.
Section ClassDef.
Record mixin_of d (T : tbDistrLatticeType d) (sub : T T T) := Mixin {
   compl : T T;
   _ : x, compl x = sub top x
}.

Record class_of (T : Type) := Class {
  base : TBDistrLattice.class_of T;
  mixin1_disp : unit;
  mixin1 : CBDistrLattice.mixin_of (BDistrLattice.Pack mixin1_disp base);
  mixin2_disp : unit;
  mixin2 : @mixin_of _ (TBDistrLattice.Pack mixin2_disp base)
                     (CBDistrLattice.sub mixin1)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack disp T c.
Definition clone_with disp' c of phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack :=
  fun bT b & phant_id (@TBDistrLattice.class disp bT) b
  fun disp1 m1T m1 & phant_id (@CBDistrLattice.class disp1 m1T)
                              (@CBDistrLattice.Class _ _ _ m1) ⇒
  fun disp2 m2Pack disp (@Class T b disp1 m1 disp2 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 distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass.
Definition cb_tbLatticeType := @TBLattice.Pack disp cbDistrLatticeType xclass.
Definition cb_tbDistrLatticeType :=
  @TBDistrLattice.Pack disp cbDistrLatticeType xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> TBDistrLattice.class_of.
Coercion base2 : class_of >-> CBDistrLattice.class_of.
Coercion mixin1 : class_of >-> CBDistrLattice.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 distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Coercion tbDistrLatticeType : type >-> TBDistrLattice.type.
Coercion cbDistrLatticeType : type >-> CBDistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Canonical tbDistrLatticeType.
Canonical cbDistrLatticeType.
Canonical cb_tbLatticeType.
Canonical cb_tbDistrLatticeType.
Notation ctbDistrLatticeType := type.
Notation ctbDistrLatticeMixin := mixin_of.
Notation CTBDistrLatticeMixin := Mixin.
Notation CTBDistrLatticeType T m := (@pack T _ _ _ id _ _ _ id _ m).
Notation "[ 'ctbDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'ctbDistrLatticeType' 'of' T 'for' cT ]") :
  form_scope.
Notation "[ 'ctbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0,
   format "[ 'ctbDistrLatticeType' 'of' T 'for' cT 'with' disp ]")
  : form_scope.
Notation "[ 'ctbDistrLatticeType' 'of' T ]" := [ctbDistrLatticeType of T for _]
  (at level 0, format "[ 'ctbDistrLatticeType' 'of' T ]") : form_scope.
Notation "[ 'ctbDistrLatticeType' 'of' T 'with' disp ]" :=
  [ctbDistrLatticeType of T for _ with disp]
  (at level 0, format "[ 'ctbDistrLatticeType' 'of' T 'with' disp ]") :
  form_scope.
Notation "[ 'default_ctbDistrLatticeType' 'of' T ]" :=
  (@pack T _ _ _ id _ _ id (Mixin (fun erefl)))
  (at level 0, format "[ 'default_ctbDistrLatticeType' 'of' T ]") :
  form_scope.
End Exports.

End CTBDistrLattice.
Export CTBDistrLattice.Exports.

Definition compl {d : unit} {T : ctbDistrLatticeType d} : T T :=
  CTBDistrLattice.compl (CTBDistrLattice.class T).

Module Import CTBDistrLatticeSyntax.
Notation "~` A" := (compl A) : order_scope.
End CTBDistrLatticeSyntax.

Module Total.
Definition mixin_of d (T : latticeType d) := total (<=%O : rel T).
Section ClassDef.

Record class_of (T : Type) := Class {
  base : DistrLattice.class_of T;
  mixin_disp : unit;
  mixin : mixin_of (DistrLattice.Pack mixin_disp base)
}.


Structure type (d : unit) := Pack { sort; _ : class_of sort }.


Variables (T : Type) (disp : unit) (cT : type disp).

Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c & phant_id class c := @Pack disp T c.
Definition clone_with disp' c & phant_id class c := @Pack disp' T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack disp0 (T0 : distrLatticeType disp0) (m0 : mixin_of T0) :=
  fun bT b & phant_id (@DistrLattice.class disp bT) b
  fun m & phant_id m0 mPack disp (@Class T b disp0 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 distrLatticeType := @DistrLattice.Pack disp cT xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> DistrLattice.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.
Coercion distrLatticeType : type >-> DistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical porderType.
Canonical latticeType.
Canonical distrLatticeType.
Notation totalOrderMixin := Total.mixin_of.
Notation orderType := type.
Notation OrderType T m := (@pack T _ _ _ m _ _ id _ id).
Notation "[ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ id)
  (at level 0, format "[ 'orderType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'orderType' 'of' T 'for' cT 'with' disp ]" :=
  (@clone_with T _ cT disp _ id)
  (at level 0, format "[ 'orderType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
Notation "[ 'orderType' 'of' T ]" := [orderType of T for _]
  (at level 0, format "[ 'orderType' 'of' T ]") : form_scope.
Notation "[ 'orderType' 'of' T 'with' disp ]" :=
  [orderType of T for _ with disp]
  (at level 0, format "[ 'orderType' 'of' T 'with' disp ]") : form_scope.
End Exports.

End Total.
Import Total.Exports.

FINITE

Module FinPOrder.
Section ClassDef.

Record class_of T := Class {
  base : POrder.class_of T;
  mixin : Finite.mixin_of (Equality.Pack base)
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@POrder.class disp bT) b
  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) ⇒
  Pack disp (@Class T b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition countType := @Countable.Pack cT xclass.
Definition finType := @Finite.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition count_porderType := @POrder.Pack disp countType xclass.
Definition fin_porderType := @POrder.Pack disp finType xclass.
End ClassDef.

Module Exports.
Coercion base : class_of >-> POrder.class_of.
Coercion base2 : class_of >-> Finite.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion countType : type >-> Countable.type.
Coercion finType : type >-> Finite.type.
Coercion porderType : type >-> POrder.type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Canonical porderType.
Canonical count_porderType.
Canonical fin_porderType.
Notation finPOrderType := type.
Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'finPOrderType' 'of' T ]") : form_scope.
End Exports.

End FinPOrder.
Import FinPOrder.Exports.

Module FinLattice.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : TBLattice.class_of T;
  mixin : Finite.mixin_of (Equality.Pack base);
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@TBLattice.class disp bT) b
  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) ⇒
  Pack disp (@Class T b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition countType := @Countable.Pack cT xclass.
Definition finType := @Finite.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
Definition count_latticeType := @Lattice.Pack disp countType xclass.
Definition count_bLatticeType := @BLattice.Pack disp countType xclass.
Definition count_tbLatticeType := @TBLattice.Pack disp countType xclass.
Definition fin_latticeType := @Lattice.Pack disp finType xclass.
Definition fin_bLatticeType := @BLattice.Pack disp finType xclass.
Definition fin_tbLatticeType := @TBLattice.Pack disp finType xclass.
Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass.
Definition finPOrder_bLatticeType := @BLattice.Pack disp finPOrderType xclass.
Definition finPOrder_tbLatticeType := @TBLattice.Pack disp finPOrderType xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> TBLattice.class_of.
Coercion base2 : class_of >-> FinPOrder.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion countType : type >-> Countable.type.
Coercion finType : type >-> Finite.type.
Coercion porderType : type >-> POrder.type.
Coercion finPOrderType : type >-> FinPOrder.type.
Coercion latticeType : type >-> Lattice.type.
Coercion bLatticeType : type >-> BLattice.type.
Coercion tbLatticeType : type >-> TBLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Canonical porderType.
Canonical finPOrderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical count_latticeType.
Canonical count_bLatticeType.
Canonical count_tbLatticeType.
Canonical fin_latticeType.
Canonical fin_bLatticeType.
Canonical fin_tbLatticeType.
Canonical finPOrder_latticeType.
Canonical finPOrder_bLatticeType.
Canonical finPOrder_tbLatticeType.
Notation finLatticeType := type.
Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'finLatticeType' 'of' T ]") : form_scope.
End Exports.

End FinLattice.
Export FinLattice.Exports.

Module FinDistrLattice.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : TBDistrLattice.class_of T;
  mixin : Finite.mixin_of (Equality.Pack base);
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@TBDistrLattice.class disp bT) b
  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) ⇒
  Pack disp (@Class T b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition countType := @Countable.Pack cT xclass.
Definition finType := @Finite.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
Definition finLatticeType := @FinLattice.Pack disp cT xclass.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
Definition count_distrLatticeType := @DistrLattice.Pack disp countType xclass.
Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType xclass.
Definition count_tbDistrLatticeType :=
  @TBDistrLattice.Pack disp countType xclass.
Definition fin_distrLatticeType := @DistrLattice.Pack disp finType xclass.
Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType xclass.
Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType xclass.
Definition finPOrder_distrLatticeType :=
  @DistrLattice.Pack disp finPOrderType xclass.
Definition finPOrder_bDistrLatticeType :=
  @BDistrLattice.Pack disp finPOrderType xclass.
Definition finPOrder_tbDistrLatticeType :=
  @TBDistrLattice.Pack disp finPOrderType xclass.
Definition finLattice_distrLatticeType :=
  @DistrLattice.Pack disp finLatticeType xclass.
Definition finLattice_bDistrLatticeType :=
  @BDistrLattice.Pack disp finLatticeType xclass.
Definition finLattice_tbDistrLatticeType :=
  @TBDistrLattice.Pack disp finLatticeType xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> TBDistrLattice.class_of.
Coercion base2 : class_of >-> FinLattice.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion countType : type >-> Countable.type.
Coercion finType : type >-> Finite.type.
Coercion porderType : type >-> POrder.type.
Coercion finPOrderType : type >-> FinPOrder.type.
Coercion latticeType : type >-> Lattice.type.
Coercion bLatticeType : type >-> BLattice.type.
Coercion tbLatticeType : type >-> TBLattice.type.
Coercion finLatticeType : type >-> FinLattice.type.
Coercion distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Coercion tbDistrLatticeType : type >-> TBDistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Canonical porderType.
Canonical finPOrderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical finLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Canonical tbDistrLatticeType.
Canonical count_distrLatticeType.
Canonical count_bDistrLatticeType.
Canonical count_tbDistrLatticeType.
Canonical fin_distrLatticeType.
Canonical fin_bDistrLatticeType.
Canonical fin_tbDistrLatticeType.
Canonical finPOrder_distrLatticeType.
Canonical finPOrder_bDistrLatticeType.
Canonical finPOrder_tbDistrLatticeType.
Canonical finLattice_distrLatticeType.
Canonical finLattice_bDistrLatticeType.
Canonical finLattice_tbDistrLatticeType.
Notation finDistrLatticeType := type.
Notation "[ 'finDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'finDistrLatticeType' 'of' T ]") : form_scope.
End Exports.

End FinDistrLattice.
Export FinDistrLattice.Exports.

Module FinCDistrLattice.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : CTBDistrLattice.class_of T;
  mixin : Finite.mixin_of (Equality.Pack base);
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@CTBDistrLattice.class disp bT) b
  fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) ⇒
  Pack disp (@Class T b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition countType := @Countable.Pack cT xclass.
Definition finType := @Finite.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
Definition finLatticeType := @FinLattice.Pack disp cT xclass.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass.
Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass.
Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT xclass.
Definition count_cbDistrLatticeType :=
  @CBDistrLattice.Pack disp countType xclass.
Definition count_ctbDistrLatticeType :=
  @CTBDistrLattice.Pack disp countType xclass.
Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType xclass.
Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType xclass.
Definition finPOrder_cbDistrLatticeType :=
  @CBDistrLattice.Pack disp finPOrderType xclass.
Definition finPOrder_ctbDistrLatticeType :=
  @CTBDistrLattice.Pack disp finPOrderType xclass.
Definition finLattice_cbDistrLatticeType :=
  @CBDistrLattice.Pack disp finLatticeType xclass.
Definition finLattice_ctbDistrLatticeType :=
  @CTBDistrLattice.Pack disp finLatticeType xclass.
Definition finDistrLattice_cbDistrLatticeType :=
  @CBDistrLattice.Pack disp finDistrLatticeType xclass.
Definition finDistrLattice_ctbDistrLatticeType :=
  @CTBDistrLattice.Pack disp finDistrLatticeType xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> CTBDistrLattice.class_of.
Coercion base2 : class_of >-> FinDistrLattice.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion countType : type >-> Countable.type.
Coercion finType : type >-> Finite.type.
Coercion porderType : type >-> POrder.type.
Coercion finPOrderType : type >-> FinPOrder.type.
Coercion latticeType : type >-> Lattice.type.
Coercion bLatticeType : type >-> BLattice.type.
Coercion tbLatticeType : type >-> TBLattice.type.
Coercion finLatticeType : type >-> FinLattice.type.
Coercion distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Coercion tbDistrLatticeType : type >-> TBDistrLattice.type.
Coercion finDistrLatticeType : type >-> FinDistrLattice.type.
Coercion cbDistrLatticeType : type >-> CBDistrLattice.type.
Coercion ctbDistrLatticeType : type >-> CTBDistrLattice.type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Canonical porderType.
Canonical finPOrderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical finLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Canonical tbDistrLatticeType.
Canonical finDistrLatticeType.
Canonical cbDistrLatticeType.
Canonical ctbDistrLatticeType.
Canonical count_cbDistrLatticeType.
Canonical count_ctbDistrLatticeType.
Canonical fin_cbDistrLatticeType.
Canonical fin_ctbDistrLatticeType.
Canonical finPOrder_cbDistrLatticeType.
Canonical finPOrder_ctbDistrLatticeType.
Canonical finLattice_cbDistrLatticeType.
Canonical finLattice_ctbDistrLatticeType.
Canonical finDistrLattice_cbDistrLatticeType.
Canonical finDistrLattice_ctbDistrLatticeType.
Notation finCDistrLatticeType := type.
Notation "[ 'finCDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id)
  (at level 0, format "[ 'finCDistrLatticeType' 'of' T ]") : form_scope.
End Exports.

End FinCDistrLattice.
Export FinCDistrLattice.Exports.

Module FinTotal.
Section ClassDef.

Record class_of (T : Type) := Class {
  base : FinDistrLattice.class_of T;
  mixin_disp : unit;
  mixin : totalOrderMixin (DistrLattice.Pack mixin_disp base)
}.


Structure type (disp : unit) := Pack { sort; _ : class_of sort }.


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 bT b & phant_id (@FinDistrLattice.class disp bT) b
  fun disp' mT m & phant_id (@Total.class disp mT) (@Total.Class _ _ _ m) ⇒
  Pack disp (@Class T b disp' m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition countType := @Countable.Pack cT xclass.
Definition finType := @Finite.Pack cT xclass.
Definition porderType := @POrder.Pack disp cT xclass.
Definition finPOrderType := @FinPOrder.Pack disp cT xclass.
Definition latticeType := @Lattice.Pack disp cT xclass.
Definition bLatticeType := @BLattice.Pack disp cT xclass.
Definition tbLatticeType := @TBLattice.Pack disp cT xclass.
Definition finLatticeType := @FinLattice.Pack disp cT xclass.
Definition distrLatticeType := @DistrLattice.Pack disp cT xclass.
Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass.
Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass.
Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass.
Definition orderType := @Total.Pack disp cT xclass.
Definition order_countType := @Countable.Pack orderType xclass.
Definition order_finType := @Finite.Pack orderType xclass.
Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass.
Definition order_bLatticeType := @BLattice.Pack disp orderType xclass.
Definition order_tbLatticeType := @TBLattice.Pack disp orderType xclass.
Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass.
Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType xclass.
Definition order_tbDistrLatticeType :=
  @TBDistrLattice.Pack disp orderType xclass.
Definition order_finDistrLatticeType :=
  @FinDistrLattice.Pack disp orderType xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> FinDistrLattice.class_of.
Coercion base2 : class_of >-> Total.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Coercion choiceType : type >-> Choice.type.
Coercion countType : type >-> Countable.type.
Coercion finType : type >-> Finite.type.
Coercion porderType : type >-> POrder.type.
Coercion finPOrderType : type >-> FinPOrder.type.
Coercion latticeType : type >-> Lattice.type.
Coercion bLatticeType : type >-> BLattice.type.
Coercion tbLatticeType : type >-> TBLattice.type.
Coercion finLatticeType : type >-> FinLattice.type.
Coercion distrLatticeType : type >-> DistrLattice.type.
Coercion bDistrLatticeType : type >-> BDistrLattice.type.
Coercion tbDistrLatticeType : type >-> TBDistrLattice.type.
Coercion finDistrLatticeType : type >-> FinDistrLattice.type.
Coercion orderType : type >-> Total.type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Canonical porderType.
Canonical finPOrderType.
Canonical latticeType.
Canonical bLatticeType.
Canonical tbLatticeType.
Canonical finLatticeType.
Canonical distrLatticeType.
Canonical bDistrLatticeType.
Canonical tbDistrLatticeType.
Canonical finDistrLatticeType.
Canonical orderType.
Canonical order_countType.
Canonical order_finType.
Canonical order_finPOrderType.
Canonical order_bLatticeType.
Canonical order_tbLatticeType.
Canonical order_finLatticeType.
Canonical order_bDistrLatticeType.
Canonical order_tbDistrLatticeType.
Canonical order_finDistrLatticeType.
Notation finOrderType := type.
Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ _ id)
  (at level 0, format "[ 'finOrderType' 'of' T ]") : form_scope.
End Exports.

End FinTotal.
Export FinTotal.Exports.

DUAL

Definition dual T : Type := T.
Definition dual_display : unit unit.

Module Import DualSyntax.

Notation "T ^d" := (dual T) (at level 2, format "T ^d") : type_scope.
Notation "<=^d%O" := (@le (dual_display _) _) : fun_scope.
Notation ">=^d%O" := (@ge (dual_display _) _) : fun_scope.
Notation ">=^d%O" := (@ge (dual_display _) _) : fun_scope.
Notation "<^d%O" := (@lt (dual_display _) _) : fun_scope.
Notation ">^d%O" := (@gt (dual_display _) _) : fun_scope.
Notation "<?=^d%O" := (@leif (dual_display _) _) : fun_scope.
Notation ">=<^d%O" := (@comparable (dual_display _) _) : fun_scope.
Notation "><^d%O" := (fun x y~~ (@comparable (dual_display _) _ x y)) :
  fun_scope.

Notation "<=^d y" := (>=^d%O y) : order_scope.
Notation "<=^d y :> T" := (<=^d (y : T)) (only parsing) : order_scope.
Notation ">=^d y" := (<=^d%O y) : order_scope.
Notation ">=^d y :> T" := (>=^d (y : T)) (only parsing) : order_scope.

Notation "<^d y" := (>^d%O y) : order_scope.
Notation "<^d y :> T" := (<^d (y : T)) (only parsing) : order_scope.
Notation ">^d y" := (<^d%O y) : order_scope.
Notation ">^d y :> T" := (>^d (y : T)) (only parsing) : order_scope.

Notation ">=<^d y" := (>=<^d%O y) : order_scope.
Notation ">=<^d y :> T" := (>=<^d (y : T)) (only parsing) : order_scope.

Notation "x <=^d y" := (<=^d%O x y) : order_scope.
Notation "x <=^d y :> T" := ((x : T) <=^d (y : T)) (only parsing) : order_scope.
Notation "x >=^d y" := (y <=^d x) (only parsing) : order_scope.
Notation "x >=^d y :> T" := ((x : T) >=^d (y : T)) (only parsing) : order_scope.

Notation "x <^d y" := (<^d%O x y) : order_scope.
Notation "x <^d y :> T" := ((x : T) <^d (y : T)) (only parsing) : order_scope.
Notation "x >^d y" := (y <^d x) (only parsing) : order_scope.
Notation "x >^d y :> T" := ((x : T) >^d (y : T)) (only parsing) : order_scope.

Notation "x <=^d y <=^d z" := ((x <=^d y) && (y <=^d z)) : order_scope.
Notation "x <^d y <=^d z" := ((x <^d y) && (y <=^d z)) : order_scope.
Notation "x <=^d y <^d z" := ((x <=^d y) && (y <^d z)) : order_scope.
Notation "x <^d y <^d z" := ((x <^d y) && (y <^d z)) : order_scope.

Notation "x <=^d y ?= 'iff' C" := (<?=^d%O x y C) : order_scope.
Notation "x <=^d y ?= 'iff' C :> T" := ((x : T) <=^d (y : T) ?= iff C)
  (only parsing) : order_scope.

Notation ">=<^d x" := (>=<^d%O x) : order_scope.
Notation ">=<^d x :> T" := (>=<^d (x : T)) (only parsing) : order_scope.
Notation "x >=<^d y" := (>=<^d%O x y) : order_scope.

Notation "><^d x" := (fun y~~ (>=<^d%O x y)) : order_scope.
Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope.
Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope.

Notation dual_bottom := (@bottom (dual_display _)).
Notation dual_top := (@top (dual_display _)).
Notation dual_join := (@join (dual_display _) _).
Notation dual_meet := (@meet (dual_display _) _).
Notation dual_max := (@max (dual_display _) _).
Notation dual_min := (@min (dual_display _) _).

Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope.
Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope.

Notation "\join^d_ ( i <- r | P ) F" :=
  (\big[join/0]_(i <- r | P%B) F%O) : order_scope.
Notation "\join^d_ ( i <- r ) F" :=
  (\big[join/0]_(i <- r) F%O) : order_scope.
Notation "\join^d_ ( i | P ) F" :=
  (\big[join/0]_(i | P%B) F%O) : order_scope.
Notation "\join^d_ i F" :=
  (\big[join/0]_i F%O) : order_scope.
Notation "\join^d_ ( i : I | P ) F" :=
  (\big[join/0]_(i : I | P%B) F%O) (only parsing) : order_scope.
Notation "\join^d_ ( i : I ) F" :=
  (\big[join/0]_(i : I) F%O) (only parsing) : order_scope.
Notation "\join^d_ ( m <= i < n | P ) F" :=
 (\big[join/0]_(m i < n | P%B) F%O) : order_scope.
Notation "\join^d_ ( m <= i < n ) F" :=
 (\big[join/0]_(m i < n) F%O) : order_scope.
Notation "\join^d_ ( i < n | P ) F" :=
 (\big[join/0]_(i < n | P%B) F%O) : order_scope.
Notation "\join^d_ ( i < n ) F" :=
 (\big[join/0]_(i < n) F%O) : order_scope.
Notation "\join^d_ ( i 'in' A | P ) F" :=
 (\big[join/0]_(i in A | P%B) F%O) : order_scope.
Notation "\join^d_ ( i 'in' A ) F" :=
 (\big[join/0]_(i in A) F%O) : order_scope.

Notation "\meet^d_ ( i <- r | P ) F" :=
  (\big[meet/1]_(i <- r | P%B) F%O) : order_scope.
Notation "\meet^d_ ( i <- r ) F" :=
  (\big[meet/1]_(i <- r) F%O) : order_scope.
Notation "\meet^d_ ( i | P ) F" :=
  (\big[meet/1]_(i | P%B) F%O) : order_scope.
Notation "\meet^d_ i F" :=
  (\big[meet/1]_i F%O) : order_scope.
Notation "\meet^d_ ( i : I | P ) F" :=
  (\big[meet/1]_(i : I | P%B) F%O) (only parsing) : order_scope.
Notation "\meet^d_ ( i : I ) F" :=
  (\big[meet/1]_(i : I) F%O) (only parsing) : order_scope.
Notation "\meet^d_ ( m <= i < n | P ) F" :=
 (\big[meet/1]_(m i < n | P%B) F%O) : order_scope.
Notation "\meet^d_ ( m <= i < n ) F" :=
 (\big[meet/1]_(m i < n) F%O) : order_scope.
Notation "\meet^d_ ( i < n | P ) F" :=
 (\big[meet/1]_(i < n | P%B) F%O) : order_scope.
Notation "\meet^d_ ( i < n ) F" :=
 (\big[meet/1]_(i < n) F%O) : order_scope.
Notation "\meet^d_ ( i 'in' A | P ) F" :=
 (\big[meet/1]_(i in A | P%B) F%O) : order_scope.
Notation "\meet^d_ ( i 'in' A ) F" :=
 (\big[meet/1]_(i in A) F%O) : order_scope.

End DualSyntax.

THEORY

Module Import POrderTheory.
Section POrderTheory.

Context {disp : unit}.
Context {T : porderType}.

Implicit Types (x y : T) (s : seq T).

Lemma geE x y : ge x y = (y x).
Lemma gtE x y : gt x y = (y < x).

Lemma lexx (x : T) : x x.
Hint Resolve lexx : core.

Definition le_refl : reflexive le := lexx.
Definition ge_refl : reflexive ge := lexx.
Hint Resolve le_refl : core.

Lemma le_anti: antisymmetric (<=%O : rel T).

Lemma ge_anti: antisymmetric (>=%O : rel T).

Lemma le_trans: transitive (<=%O : rel T).

Lemma ge_trans: transitive (>=%O : rel T).

Lemma lt_def x y: (x < y) = (y != x) && (x y).

Lemma lt_neqAle x y: (x < y) = (x != y) && (x y).

Lemma ltxx x: x < x = false.

Definition lt_irreflexive : irreflexive lt := ltxx.
Hint Resolve lt_irreflexive : core.

Definition ltexx := (lexx, ltxx).

Lemma le_eqVlt x y: (x y) = (x == y) || (x < y).

Lemma lt_eqF x y: x < y x == y = false.

Lemma gt_eqF x y : y < x x == y = false.

Lemma eq_le x y: (x == y) = (x y x).

Lemma ltW x y: x < y x y.

Lemma lt_le_trans y x z: x < y y z x < z.

Lemma lt_trans: transitive (<%O : rel T).

Lemma le_lt_trans y x z: x y y < z x < z.

Lemma lt_nsym x y : x < y y < x False.

Lemma lt_asym x y : x < y < x = false.

Lemma le_gtF x y: x y y < x = false.

Lemma lt_geF x y : (x < y) y x = false.

Definition lt_gtF x y hxy := le_gtF (@ltW x y hxy).

Lemma lt_leAnge x y : (x < y) = (x y) && ~~ (y x).

Lemma lt_le_asym x y : x < y x = false.

Lemma le_lt_asym x y : x y < x = false.

Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym).

Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s.

Lemma eq_sorted_lt s1 s2 : sorted lt s1 sorted lt s2 s1 =i s2 s1 = s2.

Lemma eq_sorted_le s1 s2 : sorted le s1 sorted le s2
  perm_eq s1 s2 s1 = s2.

Lemma comparable_leNgt x y : x >=< y (x y) = ~~ (y < x).

Lemma comparable_ltNge x y : x >=< y (x < y) = ~~ (y x).

Lemma comparable_ltgtP x y : x >=< y
  compare x y (min y x) (min x y) (max y x) (max x y)
  (y == x) (x == y) (x y) (x y) (x > y) (x < y).

Lemma comparable_leP x y : x >=< y
  le_xor_gt x y (min y x) (min x y) (max y x) (max x y) (x y) (y < x).

Lemma comparable_ltP x y : x >=< y
  lt_xor_ge x y (min y x) (min x y) (max y x) (max x y) (y x) (x < y).

Lemma comparable_sym x y : (y >=< x) = (x >=< y).

Lemma comparablexx x : x >=< x.

Lemma incomparable_eqF x y : (x >< y) (x == y) = false.

Lemma incomparable_leF x y : (x >< y) (x y) = false.

Lemma incomparable_ltF x y : (x >< y) (x < y) = false.

Lemma comparableP x y : incompare x y
  (min y x) (min x y) (max y x) (max x y)
  (y == x) (x == y) (x y) (x y) (x > y) (x < y)
  (y >=< x) (x >=< y).

Lemma le_comparable (x y : T) : x y x >=< y.

Lemma lt_comparable (x y : T) : x < y x >=< y.

Lemma ge_comparable (x y : T) : y x x >=< y.

Lemma gt_comparable (x y : T) : y < x x >=< y.

Lemma leifP x y C : reflect (x y ?= iff C) (if C then x == y else x < y).

Lemma leif_refl x C : reflect (x x ?= iff C) C.

Lemma leif_trans x1 x2 x3 C12 C23 :
  x1 x2 ?= iff C12 x2 x3 ?= iff C23 x1 x3 ?= iff C12 && C23.

Lemma leif_le x y : x y x y ?= iff (x y).

Lemma leif_eq x y : x y x y ?= iff (x == y).

Lemma ge_leif x y C : x y ?= iff C (y x) = C.

Lemma lt_leif x y C : x y ?= iff C (x < y) = ~~ C.

Lemma ltNleif x y C : x y ?= iff ~~ C (x < y) = C.

Lemma eq_leif x y C : x y ?= iff C