Library mathcomp.ssreflect.order

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

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

Types equipped with order relations NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This files defines types equipped with order relations.

How to use orders in MathComp?

Use one of the following modules implementing different theories (all located in the module Order): 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".

Interfaces

Before providing the list of interfaces, a word is necessary about "displays". Each generic partial order has, as a first argument, a display to control the printing of notations. For example, when m and n are of type natdvd (an alias of nat), (Order.le m n) is displayed m %| n; natdvd is associated to the display dvd_display. Instantiating d with tt or an unknown display will lead to a default display for notations. See below for more details about displays. We provide the following interfaces for types equipped with an order: porderType d == the type of partially ordered types The HB class is called POrder. latticeType d == the type of non-distributive lattices The HB class is called Lattice. bPOrderType d == partial order with a bottom element The HB class is called BPOrder. bLatticeType d == latticeType with a bottom element The HB class is called BLattice. tPOrderType d == partial order with a top element The HB class is called TPOrder. tbPOrderType d == partial order with a top and a bottom elements The HB class is called TBPOrder. tLatticeType d == latticeType with a top element The HB class is called TLattice. tbLatticeType d == latticeType with both a top and a bottom The HB class is called TBLattice. distrLatticeType d == the type of distributive lattices The HB class is called DistrLattice. bDistrLatticeType d == distrLatticeType with a bottom element The HB class is called BDistrLattice. tbDistrLatticeType d == distrLatticeType with both a top and a bottom The HB class is called TBDistrLattice. cbDistrLatticeType d == the type of sectionally complemented distributive lattices (lattices with bottom and a difference operation) The HB class is called CBDistrLattice. ctbDistrLatticeType d == the type of complemented distributive lattices (lattices with top, bottom, difference, and complement) The HB class is called CTBDistrLattice. orderType d == the type of totally ordered types The HB class is called Total. finPOrderType d == the type of partially ordered finite types The HB class is called FinPOrder. finLatticeType d == the type of nonempty finite non-distributive lattices The HB class is called FinLattice. finDistrLatticeType d == the type of nonempty finite distributive lattices The HB class is called FinDistrLattice. finCDistrLatticeType d == the type of nonempty finite complemented distributive lattices The HB class is called FinCDistrLattice. finOrderType d == the type of nonempty totally ordered finite types The HB class is called FinTotal. and their joins with subType: subPOrder d T P d' == join of porderType d' and subType (P : pred T) such that val is monotonic The HB class is called SubPOrder. meetSubLattice d T P d' == join of latticeType d' and subType (P : pred T) such that val is monotonic and a morphism for meet The HB class is called MeetSubLattice. joinSubLattice d T P d' == join of latticeType d' and subType (P : pred T) such that val is monotonic and a morphism for join The HB class is called JoinSubLattice. subLattice d T P d' == join of JoinSubLattice and MeetSubLattice The HB class is called SubLattice. bJoinSubLattice d T P d' == join of JoinSubLattice and BLattice such that val is a morphism for \bot The HB class is called BJoinSubLattice. tMeetSubLattice d T P d' == join of MeetSubLattice and TLattice such that val is a morphism for \top The HB class is called TMeetSubLattice. bSubLattice d T P d' == join of SubLattice and BLattice such that val is a morphism for \bot The HB class is called BSubLattice. tSubLattice d T P d' == join of SubLattice and TLattice such that val is a morphism for \top The HB class is called BSubLattice. subOrder d T P d' == join of orderType d' and subLatticeType d T P d' The HB class is called SubOrder. subPOrderLattice d T P d' == join of SubPOrder and Lattice The HB class is called SubPOrderLattice. subPOrderBLattice d T P d' == join of SubPOrder and BLattice The HB class is called SubPOrderBLattice. subPOrderTLattice d T P d' == join of SubPOrder and TLattice The HB class is called SubPOrderTLattice. subPOrderTBLattice d T P d' == join of SubPOrder and TBLattice The HB class is called SubPOrderTBLattice. meetSubBLattice d T P d' == join of MeetSubLattice and BLattice The HB class is called MeetSubBLattice. meetSubTLattice d T P d' == join of MeetSubLattice and TLattice The HB class is called MeetSubTLattice. meetSubTBLattice d T P d' == join of MeetSubLattice and TBLattice The HB class is called MeetSubTBLattice. joinSubBLattice d T P d' == join of JoinSubLattice and BLattice The HB class is called JoinSubBLattice. joinSubTLattice d T P d' == join of JoinSubLattice and TLattice The HB class is called JoinSubTLattice. joinSubTBLattice d T P d' == join of JoinSubLattice and TBLattice The HB class is called JoinSubTBLattice. subBLattice d T P d' == join of SubLattice and BLattice The HB class is called SubBLattice. subTLattice d T P d' == join of SubLattice and TLattice The HB class is called SubTLattice. subTBLattice d T P d' == join of SubLattice and TBLattice The HB class is called SubTBLattice. bJoinSubTLattice d T P d' == join of BJoinSubLattice and TBLattice The HB class is called BJoinSubTLattice. tMeetSubBLattice d T P d' == join of TMeetSubLattice and TBLattice The HB class is called TMeetSubBLattice. bSubTLattice d T P d' == join of BSubLattice and TBLattice The HB class is called BSubTLattice. tSubBLattice d T P d' == join of TSubLattice and TBLattice The HB class is called TSubBLattice. tbSubBLattice d T P d' == join of BSubLattice and TSubLattice The HB class is called TBSubLattice. Morphisms between the above structures: OrderMorphism.type d T d' T' == monotonic function between the two porder := {omorphism T -> T'} MeetLatticeMorphism.type d T d' T', JoinLatticeMorphism.type d T d' T', LatticeMorphism.type d T d' T' == monotonic function between two lattices which are morphism for meet, join, and meet/join respectively BLatticeMorphism.type d T d' T' := {blmorphism T -> T'}, TLatticeMorphism.type d T d' T' := {tlmorphism T -> T'}, TBLatticeMorphism.type d T d' T' := {tblmorphism T -> T'} == monotonic function between two lattices with bottom/top which are morphism for bottom/top Closedness predicates for the algebraic structures: meetLatticeClosed d T == predicate closed under meet on T : latticeType d The HB class is MeetLatticeClosed. joinLatticeClosed d T == predicate closed under join on T : latticeType d The HB class is JoinLatticeClosed. latticeClosed d T == predicate closed under meet and join The HB class is JoinLatticeClosed. bLatticeClosed d T == predicate that contains bottom The HB class is BLatticeClosed. tLatticeClosed d T == predicate that contains top The HB class is TLatticeClosed. tbLatticeClosed d T == predicate that contains top and bottom the HB class ie TBLatticeClosed. bJoinLatticeClosed d T == predicate that contains bottom and is closed under join The HB class is BJoinLatticeClosed. tMeetLatticeClosed d T == predicate that contains top and is closed under meet The HB class is TMeetLatticeClosed.

Useful lemmas:

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. 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 ?<= if C <-> x is smaller than y, and strictly if C is false x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)) x >< y <-> x and y are incomparable (:= ~~ x >=< y) f \min g <-> the function x |-> Order.min (f x) (g x); f \min g simplifies on application f \max g <-> the function x |-> Order.max (f x) (g x); f \max g simplifies on application For x, y of type T, where T is canonically a latticeType 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 bLatticeType d: \bot == the bottom element \join_<range> e == iterated join of a lattice with a bottom In a type T, where T is canonically a tbLatticeType d: \top == 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 [\bot, x] For x of type T, where T is canonically a ctbDistrLatticeType d: ~` x == the complement of x in [\bot, \top] 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 (<). Like each generic partial order, lattice operations symbols also have a first argument which is the display (ranged over by d of type unit), the second which is the minimal structure they operate on and then the operands. Here is the exhaustive l list of all such symbols for partial orders and lattices together with their default printed notation (as displayed by Check). For porderType T (in fun_scope): <=%O == @Order.le d T <%O == @Order.lt d T >=<%O == @Order.comparable d T >=%O == @Order.ge d T >%O == @Order.gt d T <?=%O == @Order.leif d T <?<=%O == @Order.lteif d T For latticeType T (in order_scope): x `&` y == @Order.meet d T x y x `|` y == @Order.join d T x y For bLatticeType T (in order_scope): \bot == @Order.bottom d T For tLatticeType T (in order_scope): \top == @Order.top d T For cbDistrLatticeType T (in order_scope): x `|` y == @Order.sub d T x y For ctbDistrLatticeType T (in order_scope): ~` x == @Order.compl d T x 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.
  • > patterns for contextual rewriting: leLHS := (X in (X <= _)%O)%pattern leRHS := (X in (_ <= X)%O)%pattern ltLHS := (X in (X < _)%O)%pattern ltRHS := (X in (_ < X)%O)%pattern
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: 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 {subset[d] T} := {set T} == a "copy" of set which is canonically ordered by the subset order and displayed in display d {subset T} := {subset[subset_display] T} Existing displays are either dual_display d (where d is a display), dvd_display, ring_display (from algebra/ssrnum.v 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. Beware of the asymmetry of canonical structure inference. Canonical structure inference makes it possible to infer the display associated to a type (or a named copy of a type) from the name. However, it does not help finding the named copy when the display is provided. In this sense displays are merely used to inform the user and the notation mechanism of what the inference did; they are not additional input for the inference. Alternative notation displays can be defined by : 1. declaring a new opaque definition of type unit. Using the idiom `Fact my_display : unit. Proof. exact: tt. Qed.` 2. using this symbol to tag canonical porderType structures using `HB.instance Definition _ := isPOrder.Build my_display my_type ...`, 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. We suggest the user to refer to the example of natdvd (further explained below) as guide line example to add their own displays. The following notations are provided to build substructures: [SubChoice_isSubPOrder of U by <: with disp] == [SubChoice_isSubPOrder of U by <: ] == porderType mixin for a subType whose base type is a porderType [SubPOrder_isSubLattice of U by <: with disp] == [SubPOrder_isSubLattice of U by <: ] == [SubChoice_isSubLattice of U by <: with disp] == [SubChoice_isSubLattice of U by <: ] == latticeType mixin for a subType whose base type is a latticeType and whose predicate's is a latticeClosed [SubPOrder_isBSubLattice of U by <: with disp] == [SubPOrder_isBSubLattice of U by <: ] == [SubChoice_isBSubLattice of U by <: with disp] == [SubChoice_isBSubLattice of U by <: ] == blatticeType mixin for a subType whose base type is a blatticeType and whose predicate's is both a latticeClosed and a bLatticeClosed [SubPOrder_isTSubLattice of U by <: with disp] == [SubPOrder_isTSubLattice of U by <: ] == [SubChoice_isTSubLattice of U by <: with disp] == [SubChoice_isTSubLattice of U by <: ] == tlatticeType mixin for a subType whose base type is a tlatticeType and whose predicate's is both a latticeClosed and a tLatticeClosed [SubPOrder_isTBSubLattice of U by <: with disp] == [SubPOrder_isTBSubLattice of U by <: ] == [SubChoice_isTBSubLattice of U by <: with disp] == [SubChoice_isTBSubLattice of U by <: ] == tblatticeType mixin for a subType whose base type is a tblatticeType and whose predicate's is both a latticeClosed and a tbLatticeClosed [SubLattice_isSubOrder of U by <: with disp] == [SubLattice_isSubOrder of U by <: ] == [SubPOrder_isSubOrder of U by <: with disp] == [SubPOrder_isSubOrder of U by <: ] == [SubChoice_isSubOrder of U by <: with disp] == [SubChoice_isSubOrder of U by <: ] == orderType mixin for a subType whose base type is an orderType [POrder of U by <: ] == porderType mixin for a subType whose base type is a porderType [Order of U by <: ] == orderType mixin for a subType whose base type is an orderType We provide expected instances of ordered types for bool, nat (for leq and and dvdn), 'I_n, 'I_n.+1 (with a top and bottom), nat for dvdn, T *prod[disp] T', T *lexi[disp] T', {t : T & T' x} (with lexicographic ordering), seqprod_with d T (using product order), seqlexi_with d T (with lexicographic ordering), n.-tupleprod[disp] (using product order), n.-tuplelexi[d] T (with lexicographic ordering), on {subset[disp] T} (using subset order) and all possible finite type instances. (Use `HB.about type` to discover the instances on type.) In order to get a canonical order on prod, seq, tuple or set, one may import modules DefaultProdOrder or DefaultProdLexiOrder, DefaultSeqProdOrder or DefaultSeqLexiOrder, DefaultTupleProdOrder or DefaultTupleLexiOrder, and DefaultSetSubsetOrder. We also provide specialized versions of some theorems from path.v. We provide Order.enum_val, Order.enum_rank, and Order.enum_rank_in, which are monotonous variations of enum_val, enum_rank, and enum_rank_in whenever the type is porderType, and their monotonicity is provided if this order is total. The theory is in the module Order (Order.enum_valK, Order.enum_rank_inK, etc) but Order.Enum can be imported to shorten these. We provide an opaque monotonous bijection tagnat.sig / tagnat.rank between the finite types {i : 'I_n & 'I_(p_ i)} and 'I_(\sum_i p_ i): tagnat.sig : 'I_(\sum_i p_ i) -> {i : 'I_n & 'I_(p_ i)} tagnat.rank : {i : 'I_n & 'I_(p_ i)} -> 'I_(\sum_i p_ i) tagnat.sig1 : 'I_(\sum_i p_ i) -> 'I_n tagnat.sig2 : forall p : 'I_(\sum_i p_ i), 'I_(p_ (tagnat.sig1 p)) tagnat.Rank : forall i, 'I_(p_ i) -> 'I_(\sum_i p_ i) Acknowledgments: This file is based on prior work by D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani

Set Implicit Arguments.

Declare Scope order_scope.

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 ">=< y" (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 "f \min g" (at level 50, left associativity).
Reserved Notation "f \max g" (at level 50, left associativity).

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

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

Reserved notation for lattices with bottom/top elements.
Reserved Notation "0%O" (at level 0). (* deprecated in 1.17.0 *)
Reserved Notation "1%O" (at level 0). (* deprecated in 1.17.0 *)
Reserved Notation "\bot" (at level 0).
Reserved Notation "\top" (at level 0).

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 y" (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 "x <^d y ?<= 'if' c" (at level 70, y, c at next level,
  format "x '[hv' <^d y '/' ?<= 'if' c ']'").
Reserved Notation "x <^d y ?<= 'if' c :> T" (at level 70, y, c at next level,
  format "x '[hv' <^d y '/' ?<= 'if' 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 Notation "0^d%O" (at level 0). (* deprecated in 1.17.0 *)
Reserved Notation "1^d%O" (at level 0). (* deprecated in 1.17.0 *)
Reserved Notation "\bot^d" (at level 0).
Reserved Notation "\top^d" (at level 0).

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 ']'").

Reserved Notation "'{' 'omorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'omorphism' U -> V }").
Reserved Notation "'{' 'mlmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'mlmorphism' U -> V }").
Reserved Notation "'{' 'jlmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'jlmorphism' U -> V }").
Reserved Notation "'{' 'lmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'lmorphism' U -> V }").
Reserved Notation "'{' 'blmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'blmorphism' U -> V }").
Reserved Notation "'{' 'tlmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'tlmorphism' U -> V }").
Reserved Notation "'{' 'tblmorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'tblmorphism' U -> V }").

Module Order.


#[short(type="porderType")]
HB.structure Definition POrder (d : unit) :=
  { T of Choice T & isPOrder d T }.


TODO: print nice error message when keyed type is not provided


Let le_refl : reflexive le.

Let le_anti : antisymmetric le.

Let le_trans : transitive le.

Let lt_def x y : lt x y = (y != x) && (le x y).



#[key="T"]
HB.builders Context (d : unit) (T : Type) of Lt_isPOrder d T.

Module POrderExports.
Arguments le_trans {d s} [_ _ _].
#[deprecated(since="mathcomp 2.0.0", note="Use POrder.clone instead.")]
Notation "[ 'porderType' 'of' T 'for' cT ]" := (POrder.clone _ T%type cT)
  (at level 0, format "[ 'porderType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use POrder.clone instead.")]
Notation "[ 'porderType' 'of' T 'for' cT 'with' disp ]" :=
  (POrder.clone disp T%type cT)
  (at level 0, format "[ 'porderType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use POrder.clone instead.")]
Notation "[ 'porderType' 'of' T ]" := (POrder.clone _ T%type _)
  (at level 0, format "[ 'porderType' 'of' T ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use POrder.clone instead.")]
Notation "[ 'porderType' 'of' T 'with' disp ]" := (POrder.clone disp T%type _)
  (at level 0, format "[ 'porderType' 'of' T 'with' disp ]") : form_scope.
End POrderExports.
Bind Scope order_scope with POrder.sort.

Section POrderDef.

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

Local Notation "x <= y" := (le x y) : order_scope.
Local Notation "x < y" := (lt x y) : order_scope.

Definition comparable : rel T := fun (x y : T) ⇒ (x y) || (y x).
Local Notation "x >=< y" := (comparable x y) : order_scope.
Local Notation "x >< y" := (~~ (x >=< y)) : order_scope.

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.

Definition lteif (x y : T) C := if C then x y else 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 : T) := if x < y then x else y.
Definition max (x y : T) := 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.

Lifted min/max operations.
Section LiftedPOrder.
Variable T' : Type.
Implicit Type f : T' T.
Definition min_fun f g x := min (f x) (g x).
Definition max_fun f g x := max (f x) (g x).
End LiftedPOrder.

End POrderDef.

Arguments ge {_ _}.
Arguments gt {_ _}.
Arguments min {_ _}.
Arguments max {_ _}.
Arguments comparable {_ _}.
Arguments min_fun {_ _ _} f g _ /.
Arguments max_fun {_ _ _} f g _ /.

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

Notation ">=< y" := [pred x | comparable x y] : order_scope.
Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope.
Notation "x >=< y" := (comparable x y) : order_scope.

Notation ">< y" := [pred x | ~~ comparable x y] : order_scope.
Notation ">< y :> T" := (>< (y : 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.

Notation "f \min g" := (min_fun f g) : order_scope.
Notation "f \max g" := (max_fun f g) : order_scope.

Notation leLHS := (X in (X _)%O)%pattern.
Notation leRHS := (X in (_ X)%O)%pattern.
Notation ltLHS := (X in (X < _)%O)%pattern.
Notation ltRHS := (X in (_ < X)%O)%pattern.

End POSyntax.

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

HB.mixin Record POrder_isJoinSemiLattice d (T : indexed Type) of POrder d T := { join : T -> T -> T; joinC : commutative join; joinA : associative join; le_defU : forall x y, (x <= y) = (join x y == y); }. # [short(type="joinSemiLatticeType") ] HB.structure Definition JoinSemiLattice d := { T of POrder_isJoinSemiLattice d T & POrder d T }. HB.mixin Record POrder_isMeetSemiLattice d (T : indexed Type) of POrder d T := { meet : T -> T -> T; meetC : commutative meet; meetA : associative meet; le_def : forall x y, (x <= y) = (meet x y == x); }. # [short(type="meetSemiLatticeType") ] HB.structure Definition MeetSemiLattice d := { T of POrder_isMeetSemiLattice d T & POrder d T }.
HB.builders Context d T of POrder_isLattice d T. Let le_defU : forall x y, (x <= y) = (join x y == y). Proof. Admitted. HB.instance Definition _ := @POrder_isMeetSemiLattice.Build d T meet meetC meetA le_def. HB.instance Definition _ := @POrder_isJoinSemiLattice.Build d T join joinC joinA le_defU. HB.end.

#[short(type="latticeType")]
HB.structure Definition Lattice d :=
  { T of POrder_isLattice d T & POrder d T }.

Module LatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use Lattice.clone instead.")]
Notation "[ 'latticeType' 'of' T 'for' cT ]" := (Lattice.clone _ T%type cT)
  (at level 0, format "[ 'latticeType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Lattice.clone instead.")]
Notation "[ 'latticeType' 'of' T 'for' cT 'with' disp ]" :=
  (Lattice.clone disp T%type cT)
  (at level 0, format "[ 'latticeType' 'of' T 'for' cT 'with' disp ]") :
  form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Lattice.clone instead.")]
Notation "[ 'latticeType' 'of' T ]" := (Lattice.clone _ T%type _)
  (at level 0, format "[ 'latticeType' 'of' T ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Lattice.clone instead.")]
Notation "[ 'latticeType' 'of' T 'with' disp ]" := (Lattice.clone disp T%type _)
  (at level 0, format "[ 'latticeType' 'of' T 'with' disp ]") : form_scope.
End LatticeExports.

Section LatticeDef.
Context {disp : unit} {T : latticeType disp}.

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

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

End LatticeSyntax.

#[key="T"]
HB.mixin Record hasBottom d (T : Type) of POrder d T := {
  bottom : T;
  le0x : x, bottom x;
}.
#[short(type="bPOrderType")]
HB.structure Definition BPOrder d := { T of hasBottom d T & POrder d T }.
#[short(type="bLatticeType")]
HB.structure Definition BLattice d := { T of hasBottom d T & Lattice d T }.

Module BLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use BLattice.clone instead.")]
Notation "[ 'bLatticeType' 'of' T 'for' cT ]" := (BLattice.clone _ T%type cT)
  (at level 0, format "[ 'bLatticeType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use BLattice.clone instead.")]
Notation "[ 'bLatticeType' 'of' T ]" := (BLattice.clone _ T%type _)
  (at level 0, format "[ 'bLatticeType' 'of' T ]") : form_scope.
End BLatticeExports.

Module BLatticeSyntax.
Notation "0%O" := bottom (only parsing). (* deprecated in 1.17.0 *)
Notation "\bot" := bottom : order_scope.

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

End BLatticeSyntax.

#[key="T"]
HB.mixin Record hasTop d (T : Type) of POrder d T := {
  top : T;
  lex1 : x, x top;
}.
#[short(type="tPOrderType")]
HB.structure Definition TPOrder d := { T of hasTop d T & POrder d T }.
#[short(type="tbPOrderType")]
HB.structure Definition TBPOrder d := { T of hasTop d T & BPOrder d T }.
#[short(type="tLatticeType")]
HB.structure Definition TLattice d := { T of hasTop d T & Lattice d T }.
#[short(type="tbLatticeType")]
HB.structure Definition TBLattice d := { T of BLattice d T & TLattice d T }.

Module TLatticeSyntax.

Notation "1%O" := top (only parsing). (* deprecated in 1.17.0 *)
Notation "\top" := top : order_scope.

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

End TLatticeSyntax.

#[key="T"]
HB.mixin Record Lattice_Meet_isDistrLattice d (T : Type) of Lattice d T := {
  meetUl : @left_distributive T T meet join;
}.
#[short(type="distrLatticeType")]
HB.structure Definition DistrLattice d :=
  { T of Lattice_Meet_isDistrLattice d T & Lattice d T }.

#[short(type="bDistrLatticeType")]
HB.structure Definition BDistrLattice d :=
  { T of hasBottom d T & DistrLattice d T}.

Module BDistrLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use BDistrLattice.clone instead.")]
Notation "[ 'bDistrLatticeType' 'of' T ]" := (BDistrLattice.clone _ T%type _)
  (at level 0, format "[ 'bDistrLatticeType' 'of' T ]") : form_scope.
End BDistrLatticeExports.

#[short(type="tbDistrLatticeType")]
HB.structure Definition TBDistrLattice d :=
  { T of TBLattice d T & BDistrLattice d T }.

Module TBDistrLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use TBDistrLattice.clone instead.")]
Notation "[ 'tbDistrLatticeType' 'of' T ]" := (TBDistrLattice.clone _ T%type _)
  (at level 0, format "[ 'tbDistrLatticeType' 'of' T ]") : form_scope.
End TBDistrLatticeExports.

#[key="T"]
HB.mixin Record hasRelativeComplement d (T : Type) of BDistrLattice d T := {
  diff : T T T;
  diffKI : x y, y `&` diff x y = bottom;
  joinIB : x y, (x `&` y) `|` diff x y = x
}.

#[short(type="cbDistrLatticeType")]
HB.structure Definition CBDistrLattice d :=
  { T of hasRelativeComplement d T & BDistrLattice d T }.

#[deprecated(since="mathcomp 2.0.0", note="Use diff instead.")]
Notation sub := diff.
#[deprecated(since="mathcomp 2.0.0", note="Use diffKI instead.")]
Notation subKI := diffKI.

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

#[key="T"]
HB.mixin Record hasComplement d (T : Type) of
         TBDistrLattice d T & CBDistrLattice d T := {
  compl : T T;
  complE : x : T, compl x = (top : T) `\` x (* FIXME? *)
}.

#[short(type="ctbDistrLatticeType")]
HB.structure Definition CTBDistrLattice d :=
  { T of hasComplement d T & TBDistrLattice d T & CBDistrLattice d T }.

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


#[short(type="orderType")]
HB.structure Definition Total d :=
  { T of DistrLattice_isTotal d T & DistrLattice d T }.

FINITE

#[short(type="finPOrderType")]
HB.structure Definition FinPOrder d := { T of Finite T & POrder d T }.

Module FinPOrderExports.
#[deprecated(since="mathcomp 2.0.0", note="Use BLattice.clone instead.")]
Notation "[ 'finPOrderType' 'of' T ]" := (FinPOrder.clone _ T%type _ )
  (at level 0, format "[ 'finPOrderType' 'of' T ]") : form_scope.
End FinPOrderExports.

#[short(type="finLatticeType")]
HB.structure Definition FinLattice d := { T of Finite T & TBLattice d T }. (* FIXME *)

Module FinLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use FinLattice.clone instead.")]
Notation "[ 'finLatticeType' 'of' T ]" := (FinLattice.clone _ T%type _ )
  (at level 0, format "[ 'finLatticeType' 'of' T ]") : form_scope.
End FinLatticeExports.

#[short(type="finDistrLatticeType")]
HB.structure Definition FinDistrLattice d :=
  { T of Finite T & TBDistrLattice d T }.

Module FinDistrLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use FinDistrLattice.clone instead.")]
Notation "[ 'finDistrLatticeType' 'of' T ]" := (FinDistrLattice.clone _ T%type _ )
  (at level 0, format "[ 'finDistrLatticeType' 'of' T ]") : form_scope.
End FinDistrLatticeExports.

#[short(type="finCDistrLatticeType")]
HB.structure Definition FinCDistrLattice d :=
  { T of Finite T & CTBDistrLattice d T }.

Module FinCDistrLatticeExports.
#[deprecated(since="mathcomp 2.0.0", note="Use FinCDistrLattice.clone instead.")]
Notation "[ 'finCDistrLatticeType' 'of' T ]" := (FinCDistrLattice.clone _ T%type _ )
  (at level 0, format "[ 'finCDistrLatticeType' 'of' T ]") : form_scope.
End FinCDistrLatticeExports.

#[short(type="finOrderType")]
HB.structure Definition FinTotal d :=
  { T of Total d T & FinDistrLattice d T }.

Module FinTotalExports.
#[deprecated(since="mathcomp 2.0.0", note="Use FinTotal.clone instead.")]
Notation "[ 'finOrderType' 'of' T ]" := (FinTotal.clone _ T%type _ )
  (at level 0, format "[ 'finOrderType' 'of' T ]") : form_scope.
End FinTotalExports.

DUAL

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

Notation dual_le := (@le (dual_display _) _).
Notation dual_lt := (@lt (dual_display _) _).
Notation dual_comparable := (@comparable (dual_display _) _).
Notation dual_ge := (@ge (dual_display _) _).
Notation dual_gt := (@gt (dual_display _) _).
Notation dual_leif := (@leif (dual_display _) _).
Notation dual_lteif := (@lteif (dual_display _) _).
Notation dual_max := (@max (dual_display _) _).
Notation dual_min := (@min (dual_display _) _).
Notation dual_meet := (@meet (dual_display _) _).
Notation dual_join := (@join (dual_display _) _).
Notation dual_bottom := (@bottom (dual_display _) _).
Notation dual_top := (@top (dual_display _) _).

Module Import DualSyntax.

Notation "T ^d" := (dual T) (at level 2, format "T ^d") : type_scope.
Notation "<=^d%O" := dual_le : fun_scope.
Notation ">=^d%O" := dual_ge : fun_scope.
Notation "<^d%O" := dual_lt : fun_scope.
Notation ">^d%O" := dual_gt : fun_scope.
Notation "<?=^d%O" := dual_leif : fun_scope.
Notation "<?<=^d%O" := dual_lteif : fun_scope.
Notation ">=<^d%O" := dual_comparable : fun_scope.
Notation "><^d%O" := (fun x y~~ dual_comparable 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 "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 "x <^d y ?<= 'if' C" := (<?<=^d%O x y C) : order_scope.
Notation "x <^d y ?<= 'if' C :> T" := ((x : T) <^d (y : T) ?<= if C)
  (only parsing) : order_scope.

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

Notation "><^d y" := [pred x | ~~ dual_comparable x 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" := (dual_meet x y) : order_scope.
Notation "x `|^d` y" := (dual_join x y) : order_scope.

Notation "0^d%O" := dual_bottom (only parsing). (* deprecated in 1.17.0 *)
Notation "1^d%O" := dual_top (only parsing). (* deprecated in 1.17.0 *)
Notation "\bot^d" := dual_bottom : order_scope.
Notation "\top^d" := dual_top : order_scope.

The following Local Notations are here to define the \join^d_ and \meet^d_ notations later. Do not remove them.
Local Notation "\bot" := dual_bottom.
Local Notation "\top" := dual_top.
Local Notation join := dual_join.
Local Notation meet := dual_meet.

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

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

End DualSyntax.

THEORY

Module Import POrderTheory.
Section POrderTheory.

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

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 le_le_trans x y z t : z x y t x y z 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 le_path_min x s : path <=%O x s all ( x) s.

Lemma lt_path_min x s : path <%O x s all (> x) s.

Lemma le_path_sortedE x s : path <=%O x s = all ( x) s && sorted <=%O s.

Lemma lt_path_sortedE x s : path <%O x s = all (> x) s && sorted <%O s.

Lemma le_sorted_pairwise s : sorted <=%O s = pairwise <=%O s.

Lemma lt_sorted_pairwise s : sorted <%O s = pairwise <%O s.

Lemma le_path_pairwise x s : path <=%O x s = pairwise <=%O (x :: s).

Lemma lt_path_pairwise x s : path <%O x s = pairwise <%O (x :: s).

Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s.

Lemma le_sorted_mask m s : sorted <=%O s sorted <=%O (mask m s).

Lemma lt_sorted_mask m s : sorted <%O s sorted <%O (mask m s).

Lemma le_sorted_filter a s : sorted <=%O s sorted <=%O (filter a s).

Lemma lt_sorted_filter a s : sorted <%O s sorted <%O (filter a s).

Lemma le_path_mask x m s : path <=%O x s path <=%O x (mask m s).

Lemma lt_path_mask x m s : path <%O x s path <%O x (mask m s).

Lemma le_path_filter x a s : path <=%O x s path <=%O x (filter a s).

Lemma lt_path_filter x a s : path <%O x s path <%O x (filter a s).

Lemma le_sorted_ltn_nth (x0 : T) (s : seq T) : sorted <=%O s
 {in [pred n | (n < size s)%N] &,
    {homo nth x0 s : i j / (i < j)%N >-> i j}}.

Lemma le_sorted_leq_nth (x0 : T) (s : seq T) : sorted <=%O s
  {in [pred n | (n < size s)%N] &,
    {homo nth x0 s : i j / (i j)%N >-> i j}}.

Lemma lt_sorted_leq_nth (x0 : T) (s : seq T) : sorted <%O s
  {in [pred n | (n < size s)%N] &,
    {mono nth x0 s : i j / (i j)%N >-> i j}}.

Lemma lt_sorted_ltn_nth (x0 : T) (s : seq T) : sorted <%O s
  {in [pred n | (n < size s)%N] &,
    {mono nth x0 s : i j / (i < j)%N >-> i < j}}.

Lemma subseq_le_path x s1 s2 : subseq s1 s2 path <=%O x s2 path <=%O x s1.

Lemma subseq_lt_path x s1 s2 : subseq s1 s2 path <%O x s2 path <%O x s1.

Lemma subseq_le_sorted s1 s2 : subseq s1 s2 sorted <=%O s2 sorted <=%O s1.

Lemma subseq_lt_sorted s1 s2 : subseq s1 s2 sorted <%O s2 sorted <%O s1.

Lemma lt_sorted_uniq s : sorted <%O s uniq s.

Lemma lt_sorted_eq s1 s2 :
  sorted <%O s1 sorted <%O s2 s1 =i s2 s1 = s2.

Lemma le_sorted_eq s1 s2 :
  sorted <=%O s1 sorted <=%O s2 perm_eq s1 s2 s1 = s2.

Lemma filter_lt_nth x0 s i : sorted <%O s (i < size s)%N
  [seq x <- s | x < nth x0 s i] = take i s.

Lemma count_lt_nth x0 s i : sorted <%O s (i < size s)%N
  count (< nth x0 s i) s = i.

Lemma filter_le_nth x0 s i : sorted <%O s (i < size s)%N
  [seq x <- s | x nth x0 s i] = take i.+1 s.

Lemma count_le_nth x0 s i : sorted <%O s (i < size s)%N
  count ( nth x0 s i) s = i.+1.

Lemma count_lt_le_mem x s : (count (< x) s < count ( x) s)%N = (x \in s).

Lemma sorted_filter_lt x s :
  sorted <=%O s [seq y <- s | y < x] = take (count (< x) s) s.

Lemma sorted_filter_le x s :
  sorted <=%O s [seq y <- s | y x] = take (count ( x) s) s.

Lemma nth_count_le x x0 s i : sorted <=%O s
  (i < count ( x) s)%N nth x0 s i x.

Lemma nth_count_lt x x0 s i : sorted <=%O s
  (i < count (< x) s)%N nth x0 s i < x.

Lemma sort_le_id s : sorted <=%O s sort <=%O s = s.

Lemma sort_lt_id s : sorted <%O s sort <%O s = s.

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.

leif

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 (x == y) = C.

Lemma eqTleif x y C : x y ?= iff C C x = y.

lteif

Lemma lteif_trans x y z C1 C2 :
  x < y ?<= if C1 y < z ?<= if C2 x < z ?<= if C1 && C2.

Lemma lteif_anti C1 C2 x y :
  (x < y ?<= if C1) && (y < x ?<= if C2) = C1 && C2 && (x == y).

Lemma lteifxx x C : (x < x ?<= if C) = C.

Lemma lteifNF x y C : y < x ?<= if ~~ C x < y ?<= if C = false.

Lemma lteifS x y C : x < y x < y ?<= if C.

Lemma lteifT x y : x < y ?<= if true = (x y).

Lemma lteifF x y : x < y ?<= if false = (x < y).

Lemma lteif_orb x y : {morph lteif x y : p q / p || q}.

Lemma lteif_andb x y : {morph lteif x y : p q / p && q}.

Lemma lteif_imply C1 C2 x y : C1 ==> C2 x < y ?<= if C1 x < y ?<= if C2.

Lemma lteifW C x y : x < y ?<= if C x y.

Lemma ltrW_lteif C x y : x < y x < y ?<= if C.

Lemma lteifN C x y : x < y ?<= if ~~ C ~~ (y < x ?<= if C).

min and max

Lemma minElt x y : min x y = if x < y then x else y.
Lemma maxElt x y : max x y = if x < y then y else x.

Lemma minEle x y : min x y = if x y then x else y.

Lemma maxEle x y : max x y = if x y then y else x.

Lemma comparable_minEgt x y : x >=< y min x y = if x > y then y else x.
Lemma comparable_maxEgt x y : x >=< y max x y = if x > y then x else y.
Lemma comparable_minEge x y : x >=< y min x y = if x y then y else x.
Lemma comparable_maxEge x y : x >=< y max x y = if x y then x else y.

Lemma min_l x y : x y min x y = x.
Lemma min_r x y : y x min x y = y.
Lemma max_l x y : y x max x y = x.
Lemma max_r x y : x y max x y = y.

Lemma minxx : idempotent (min : T T T).

Lemma maxxx : idempotent (max : T T T).

Lemma eq_minl x y : (min x y == x) = (x y).

Lemma eq_maxr x y : (max x y == y) = (x y).

Lemma min_idPl x y : reflect (min x y = x) (x y).

Lemma max_idPr x y : reflect (max x y = y) (x y).

Lemma min_minKx x y : min (min x y) y = min x y.

Lemma min_minxK x y : min x (min x y) = min x y.

Lemma max_maxKx x y : max (max x y) y = max x y.

Lemma max_maxxK x y : max x (max x y) = max x y.

Lemma comparable_minl z : {in >=< z &, x y, min x y >=< z}.

Lemma comparable_minr z : {in >=<%O z &, x y, z >=< min x y}.

Lemma comparable_maxl z : {in >=< z &, x y, max x y >=< z}.

Lemma comparable_maxr z : {in >=<%O z &, x y, z >=< max x y}.

Section Comparable2.
Variables (z x y : T) (cmp_xy : x >=< y).

Lemma comparable_minC : min x y = min y x.

Lemma comparable_maxC : max x y = max y x.

Lemma comparable_eq_minr : (min x y == y) = (y x).

Lemma comparable_eq_maxl : (max x y == x) = (y x).

Lemma comparable_min_idPr : reflect (min x y = y) (y x).

Lemma comparable_max_idPl : reflect (max x y = x) (y x).

Lemma comparable_le_min : (z min x y) = (z x) && (z y).

Lemma comparable_ge_min : (min x y z) = (x z) || (y z).

Lemma comparable_lt_min : (z < min x y) = (z < x) && (z < y).

Lemma comparable_gt_min : (min x y < z) = (x < z) || (y < z).

Lemma comparable_le_max : (z max x y) = (z x) || (z y).

Lemma comparable_ge_max : (max x y z) = (x z) && (y z).

Lemma comparable_lt_max : (z < max x y) = (z < x) || (z < y).

Lemma comparable_gt_max : (max x y < z) = (x < z) && (y < z).

Lemma comparable_minxK : max (min x y) y = y.

Lemma comparable_minKx : max x (min x y) = x.

Lemma comparable_maxxK : min (max x y) y = y.

Lemma comparable_maxKx : min x (max x y) = x.

Lemma comparable_lteifNE C : x >=< y x < y ?<= if ~~ C = ~~ (y < x ?<= if C).

Lemma comparable_lteif_minr C :
  (z < Order.min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C).

Lemma comparable_lteif_minl C :
  (Order.min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C).

Lemma comparable_lteif_maxr C :
  (z < Order.max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C).

Lemma comparable_lteif_maxl C :
  (Order.max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C).

End Comparable2.

Section Comparable3.
Variables (x y z : T) (cmp_xy : x >=< y) (cmp_xz : x >=< z) (cmp_yz : y >=< z).
Let P := comparableP.

Lemma comparable_minA : min x (min y z) = min (min x y) z.

Lemma comparable_maxA : max x (max y z) = max (max x y) z.

Lemma comparable_max_minl : max (min x y) z = min (max x z) (max y z).

Lemma comparable_min_maxl : min (max x y) z = max (min x z) (min y z).

End Comparable3.

Lemma comparable_minAC x y z : x >=< y x >=< z y >=< z
  min (min x y) z = min (min x z) y.

Lemma comparable_maxAC x y z : x >=< y x >=< z y >=< z
  max (max x y) z = max (max x z) y.

Lemma comparable_minCA x y z : x >=< y x >=< z y >=< z
  min x (min y z) = min y (min x z).

Lemma comparable_maxCA x y z : x >=< y x >=< z y >=< z
  max x (max y z) = max y (max x z).

Lemma comparable_minACA x y z t :
    x >=< y x >=< z x >=< t y >=< z y >=< t z >=< t
  min (min x y) (min z t) = min (min x z) (min y t).

Lemma comparable_maxACA x y z t :
    x >=< y x >=< z x >=< t y >=< z y >=< t z >=< t
  max (max x y) (max z t) = max (max x z) (max y t).

Lemma comparable_max_minr x y z : x >=< y x >=< z y >=< z
  max x (min y z) = min (max x y) (max x z).

Lemma comparable_min_maxr x y z : x >=< y x >=< z y >=< z
  min x (max y z) = max (min x y) (min x z).

Section ArgExtremum.

Context (I : finType) (i0 : I) (P : {pred I}) (F : I T) (Pi0 : P i0).
Hypothesis F_comparable : {in P &, i j, F i >=< F j}.

Lemma comparable_arg_minP: extremum_spec <=%O P F (arg_min i0 P F).

Lemma comparable_arg_maxP: extremum_spec >=%O P F (arg_max i0 P F).

End ArgExtremum.

monotonicity

Lemma mono_in_leif (A : {pred T}) (f : T T) C :
   {in A &, {mono f : x y / x y}}
  {in A &, x y, (f x f y ?= iff C) = (x y ?= iff C)}.

Lemma mono_leif (f : T T) C :
    {mono f : x y / x y}
   x y, (f x f y ?= iff C) = (x y ?= iff C).

Lemma nmono_in_leif (A : {pred T}) (f : T T) C :
    {in A &, {mono f : x y /~ x y}}
  {in A &, x y, (f x f y ?= iff C) = (y x ?= iff C)}.

Lemma nmono_leif (f : T T) C : {mono f : x y /~ x y}
   x y, (f x f y ?= iff C) = (y x ?= iff C).

Lemma comparable_bigl x x0 op I (P : pred I) F (s : seq I) :