Library mathcomp.order.preorder

(* (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 file and order.v define types equipped with order relations.

How to use preorders in MathComp?

Use the module PreorderTheory implementing the theories (located in the module Order):$ To access the definitions, notations, and the theory from, say, "Order.Xyz", insert "Import Order.Xyz." at the top of your scripts. You can also "Import Order.Def." to enjoy shorter notations (e.g., min instead of Order.min, nondecreasing instead of Order.nondecreasing, etc.). In order to reason about abstract orders, notations are accessible by opening the scope "order_scope" bound to the delimiting key "O"; however, when dealing with another notation scope providing order notations for a concrete instance (e.g., "ring_scope"), it is not recommended to open "order_scope" at the same time.

Control of inference (parsing) and printing

One characteristic of ordered types is that one carrier type may have several orders. For example, natural numbers can be totally or partially ordered by the less than or equal relation, the divisibility relation, and their dual relations. Therefore, we need a way to control inference of ordered type instances and printing of generic relations and operations on ordered types. As a rule of thumb, we use the carrier type or its "alias" (named copy) to control inference (using canonical structures), and use a "display" to control the printing of notations. Each generic interface and operation for ordered types has, as its first argument, a "display" of type Order.disp_t. For example, the less than or equal relation has type: Order.le : forall {d : Order.disp_t} {T : porderType d}, rel T, where porderType d is the structure of partially ordered types with display d. (@Order.le dvd_display _ m n) is printed as m %| n because ordered type instances associated to the display dvd_display is intended to represent natural numbers partially ordered by the divisibility relation. We stress that order structure inference can be triggered only from the carrier type (or its alias), but not the display. For example, writing m %| n for m and n of type nat does not trigger an inference of the divisibility relation on natural numbers, which is associated to an alias natdvd for nat; such an inference should be triggered through the use of the corresponding alias, i.e., (m : natdvd) %| n. In other words, 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. See below for various aliases and their associated displays. NB: algebra/ssrnum.v provides the display ring_display to change the scope of the usual notations to ring_scope. Instantiating d with Disp tt tt or an unknown display will lead to a default display for notations. Alternative notation displays can be defined by : 1. declaring a new opaque definition of type unit. Using the idiom `Fact my_display : Order.disp_t. Proof. exact: Disp tt 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 below as a guideline example to add their own displays.

Interfaces

We provide the following interfaces for types equipped with an order: preorderType d == the type of preordered types The HB class is called Preorder. bPreorderType d == preorderType with a bottom element (\bot) The HB class is called BPreorder. tPreorderType d == preorderType with a top element (\top) The HB class is called TPreorder. tbPreorderType d == preorderType with both a top and a bottom The HB class is called TBPreorder. finPreorderType d == the type of partially preordered finite types The HB class is called FinPreorder. finBPreorderType d == finPreorderType with a bottom element The HB class is called FinBPreorder. finTPreorderType d == finPreorderType with a top element The HB class is called FinTPreorder. finTBPreorderType d == finPreorderType with both a top and a bottom The HB class is called FinTBPreorder. and their joins with subType: subPreorder d T P d' == join of preorderType d' and subType (P : pred T) such that val is monotonic The HB class is called SubPreorder. Morphisms between the above structures: OrderMorphism.type d T d' T' == nondecreasing function between the two preorder := {omorphism T -> T'} TODO: Check this section * Useful lemmas: On orderType, leP, ltP, and 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.

Order relations and operations:

In general, an overloaded relation or operation on ordered types takes the following arguments: 1. a display d of type Order.disp_t, 2. an instance T of the minimal structure it operates on, and 3. operands. Here is the exhaustive list of all such operations together with their default notation (defined in order_scope unless specified otherwise). For T of type preorderType d, x and y of type T, and C of type bool: x <= y := @Order.le d T x y <-> x is less than or equal to y. x < y := @Order.lt d T x y <-> x is less than y, i.e., (y != x) && (x <= y). x >= y := y <= x <-> x is greater than or equal to y. x > y := y < x <-> x is greater than y. x >=< y := @Order.comparable d T x y (:= (x <= y) || (y <= x)) <-> x and y are comparable. x >< y := ~~ x >=< y <-> x and y are incomparable. x <= y ?= iff C := @Order.leif d T x y C (:= (x <= y) * ((x == y) = C)) <-> x is less than y, or equal iff C is true. x < y ?<= if C := @Order.lteif d T x y C (:= if C then x <= y else x < y) <-> x is smaller than y, and strictly if C is false. Order.min x y := if x < y then x else y Order.max x y := if x < y then y else x 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. nondecreasing f <-> the function f : T -> T' is nondecreasing, where T and T' are porderType := {homo f : x y / x <= y} Unary (partially applied) versions of order notations: >= y := @Order.le d T y == a predicate characterizing elements greater than or equal to y > y := @Order.lt d T y <= y := @Order.ge d T y < y := @Order.gt d T y >=< y := [pred x | @Order.comparable d T x y] >< y := [pred x | ~~ @Order.comparable d T x y] 0-ary versions of order notations (in function_scope): <=%O := @Order.le d T <%O := @Order.lt d T >=%O := @Order.ge d T >%O := @Order.gt d T >=<%O := @Order.comparable d T <?=%O := @Order.leif d T <?<=%O := @Order.lteif d T

> These conventions are compatible with Haskell's, where ((< y) x) = (x < y) = ((<) x y), except that we write <%O instead of (<).

For T of type bPreorderType d: \bot := @Order.bottom d T == the bottom element of type T For T of type tPreorderType d: \top := @Order.top d T == the top element of type T For preorderType 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

We provide aliases for various types and their displays: natdvd := nat (associated with display dvd_display) == an alias for 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) (associated with dual_display d where d is a display) == an alias for 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' == an alias for 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 d d' ] T' where d and d' are the displays of T and T', respectively, and prod_display adds an extra ^p to all notations T *lexi[d] T' := T * T' == an alias for 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 d d' ] T' where d and d' are the displays of T and T', respectively, and lexi_display adds an extra ^l to all notations seqprod_with d T := seq T == an alias for 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 (seqprod_display d) T where d is the display of T, and seqprod_display adds an extra ^sp to all notations n.-tupleprod T := n.-tuple[seqprod_display d] T where d is the display of T seqlexi_with d T := seq T == an alias for 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 (seqlexi_display d) T where d is the display of T, and seqlexi_display adds an extra ^sl to all notations n.-tuplelexi T := n.-tuple[seqlexi_display d] T where d is the display of T {subset[d] T} := {set T} == an alias for set which is canonically ordered by the subset order and displayed in display d {subset T} := {subset[subset_display] T} The following notations are provided to build substructures: [SubChoice_isSubPreorder of U by <: with disp] == [SubChoice_isSubPreorder of U by <: ] == preorderType mixin for a subType whose base type is a preorderType 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 monotonic 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" (c at next level,
format "x '[hv' < y '/' ?<= 'if' c ']'").
Reserved Notation "x < y ?<= 'if' c :> T" (
format "x '[hv' < y '/' ?<= 'if' c :> T ']'").

Reserved notations for bottom/top elements

Reserved Notation "\bot".
Reserved Notation "\top".

Reserved notations for dual 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 "\bot^d".
Reserved Notation "\top^d".

Reserved notations for product ordering of prod

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 "\bot^p".
Reserved Notation "\top^p".

Reserved notations for product ordering of seq

Reserved Notation "x <=^sp y" (at level 70, y at next level).
Reserved Notation "x >=^sp y" (at level 70, y at next level).
Reserved Notation "x <^sp y" (at level 70, y at next level).
Reserved Notation "x >^sp y" (at level 70, y at next level).
Reserved Notation "x <=^sp y :> T" (at level 70, y at next level).
Reserved Notation "x >=^sp y :> T" (at level 70, y at next level).
Reserved Notation "x <^sp y :> T" (at level 70, y at next level).
Reserved Notation "x >^sp y :> T" (at level 70, y at next level).
Reserved Notation "<=^sp y" (at level 35).
Reserved Notation ">=^sp y" (at level 35).
Reserved Notation "<^sp y" (at level 35).
Reserved Notation ">^sp y" (at level 35).
Reserved Notation "<=^sp y :> T" (at level 35, y at next level).
Reserved Notation ">=^sp y :> T" (at level 35, y at next level).
Reserved Notation "<^sp y :> T" (at level 35, y at next level).
Reserved Notation ">^sp y :> T" (at level 35, y at next level).
Reserved Notation "x >=<^sp y" (at level 70, no associativity).
Reserved Notation ">=<^sp x" (at level 35).
Reserved Notation ">=<^sp y :> T" (at level 35, y at next level).
Reserved Notation "x ><^sp y" (at level 70, no associativity).
Reserved Notation "><^sp x" (at level 35).
Reserved Notation "><^sp y :> T" (at level 35, y at next level).

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

Reserved Notation "\bot^sp".
Reserved Notation "\top^sp".

Reserved notations for lexicographic ordering of prod

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 Notation "\bot^l".
Reserved Notation "\top^l".

Reserved notations for lexicographic ordering of seq

Reserved Notation "x <=^sl y" (at level 70, y at next level).
Reserved Notation "x >=^sl y" (at level 70, y at next level).
Reserved Notation "x <^sl y" (at level 70, y at next level).
Reserved Notation "x >^sl y" (at level 70, y at next level).
Reserved Notation "x <=^sl y :> T" (at level 70, y at next level).
Reserved Notation "x >=^sl y :> T" (at level 70, y at next level).
Reserved Notation "x <^sl y :> T" (at level 70, y at next level).
Reserved Notation "x >^sl y :> T" (at level 70, y at next level).
Reserved Notation "<=^sl y" (at level 35).
Reserved Notation ">=^sl y" (at level 35).
Reserved Notation "<^sl y" (at level 35).
Reserved Notation ">^sl y" (at level 35).
Reserved Notation "<=^sl y :> T" (at level 35, y at next level).
Reserved Notation ">=^sl y :> T" (at level 35, y at next level).
Reserved Notation "<^sl y :> T" (at level 35, y at next level).
Reserved Notation ">^sl y :> T" (at level 35, y at next level).
Reserved Notation "x >=<^sl y" (at level 70, no associativity).
Reserved Notation ">=<^sl x" (at level 35).
Reserved Notation ">=<^sl y :> T" (at level 35, y at next level).
Reserved Notation "x ><^sl y" (at level 70, no associativity).
Reserved Notation "><^sl x" (at level 35).
Reserved Notation "><^sl y :> T" (at level 35, y at next level).

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

Reserved Notation "\bot^sl".
Reserved Notation "\top^sl".

Reserved notations for divisibility

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

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

Reserved Notation "\max_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \max_ i '/ ' F ']'").
Reserved Notation "\max_ ( i <- r | P ) F"
  (F at level 41, i, r at level 60,
           format "'[' \max_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i <- r ) F"
  (F at level 41,
           format "'[' \max_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \max_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \max_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max_ ( i | P ) F"
  (F at level 41,
           format "'[' \max_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\max_ ( i : t ) F" (F at level 41).
Reserved Notation "\max_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \max_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i < n ) F"
  (F at level 41,
           format "'[' \max_ ( i < n ) F ']'").
Reserved Notation "\max_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \max_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \max_ ( 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"
  (F at level 41, i, r at level 60,
           format "'[' \min^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i <- r ) F"
  (F at level 41, r at level 60,
           format "'[' \min^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min^d_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \min^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \min^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i | P ) F"
  (F at level 41,
           format "'[' \min^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\min^d_ ( i : t ) F" (F at level 41).
Reserved Notation "\min^d_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \min^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i < n ) F"
  (F at level 41,
           format "'[' \min^d_ ( i < n ) F ']'").
Reserved Notation "\min^d_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \min^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min^d_ ( i 'in' A ) F"
  (F at level 41,
           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"
  (F at level 41, i, r at level 60,
           format "'[' \max^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i <- r ) F"
  (F at level 41, r at level 60,
           format "'[' \max^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max^d_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \max^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \max^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i | P ) F"
  (F at level 41,
           format "'[' \max^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\max^d_ ( i : t ) F" (F at level 41).
Reserved Notation "\max^d_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \max^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i < n ) F"
  (F at level 41,
           format "'[' \max^d_ ( i < n ) F ']'").
Reserved Notation "\max^d_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \max^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max^d_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \max^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "'{' 'omorphism' U '->' V '}'"
  (at level 0, U at level 98, V at level 99,
   format "{ 'omorphism' U -> V }").

Module Order.

#[projections(primitive)] Record disp_t := Disp {d1 : unit; d2 : unit}.

#[key ="T", primitive ]
HB.mixin Record isDuallyPreorder (d : disp_t ) T of Equality T := {
  le : rel T ;
  lt : rel T ;
  lt_def : ∀ x y , lt x y = (le x y ) && ~~ (le y x );
  gt_def : ∀ x y , lt y x = (le y x ) && ~~ (le x y );
  le_refl : reflexive le ;
  ge_refl : reflexive (fun x y ⇒ le y x );
  le_trans : transitive le ;
  ge_trans : transitive (fun x y ⇒ le y x );
}.

#[short (type ="preorderType")]
HB.structure Definition Preorder (d : disp_t ) :=
  { T of Choice T & isDuallyPreorder d T }.

#[key ="T", primitive ]
HB.mixin Record hasBottom d T of Preorder d T := {
  bottom : T ;
  le0x : ∀ x , le bottom x ;
}.

#[key ="T", primitive ]
HB.mixin Record hasTop d T of Preorder d T := {
  top : T ;
  lex1 : ∀ x , le x top ;
}.

#[short (type ="bPreorderType")]
HB.structure Definition BPreorder d := { T of hasBottom d T & Preorder d T }.
#[short (type ="tPreorderType")]
HB.structure Definition TPreorder d := { T of hasTop d T & Preorder d T }.
#[short (type ="tbPreorderType")]
HB.structure Definition TBPreorder d := { T of hasTop d T & BPreorder d T }.

Section PreorderDef.

Variable (disp : disp_t) (T : preorderType 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 LiftedPreorder.
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 LiftedPreorder.

Definition nondecreasing disp' (T' : preorderType disp') (f : T → T') : Prop :=
  {homo f : x y / x ≤ y }.

End PreorderDef.

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

Module Import Def.

Notation nondecreasing := nondecreasing.
Notation min := min.
Notation max := max.

End Def.

Module Import PreOSyntax.

Notation "<=%O" := le : function_scope.
Notation ">=%O" := ge : function_scope.
Notation "<%O" := lt : function_scope.
Notation ">%O" := gt : function_scope.
Notation "<?=%O" := leif : function_scope.
Notation "<?<=%O" := lteif : function_scope.
Notation ">=<%O" := comparable : function_scope.
Notation "><%O" := (fun x y ⇒ ~~ (comparable x y )) : function_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 i ⇒ P%B) (fun i ⇒ F))
  (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]
  (format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope.

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

Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
     (arg_max i0 (fun i ⇒ P%B) (fun i ⇒ F))
  (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]
  (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]
  (i, i0 at level 10,
   format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope.

Notation "f \min g" := (min_fun f g) : function_scope.
Notation "f \max g" := (max_fun f g) : function_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.

Notation "\bot" := bottom : order_scope.
Notation "\top" := top : order_scope.

End PreOSyntax.

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

FINITE

#[short (type ="finPreorderType")]
HB.structure Definition FinPreorder d := { T of Finite T & Preorder d T }.

#[short (type ="finBPreorderType")]
HB.structure Definition FinBPreorder d := { T of FinPreorder d T & hasBottom d T }.

#[short (type ="finTPreorderType")]
HB.structure Definition FinTPreorder d := { T of FinPreorder d T & hasTop d T }.

#[short (type ="finTBPreorderType")]
HB.structure Definition FinTBPreorder d := { T of FinBPreorder d T & hasTop d T }.

DUAL

Definition dual T : Type := T.
Definition dual_display (d : disp_t) := {| d1 := d2 d; d2 := d1 d |}.

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_bottom := (@bottom (dual_display _) _).
Notation dual_top := (@top (dual_display _) _).

Module Import DualSyntax.

Notation "T ^d" := (dual T) (format "T ^d") : type_scope.
Notation "<=^d%O" := dual_le : function_scope.
Notation ">=^d%O" := dual_ge : function_scope.
Notation "<^d%O" := dual_lt : function_scope.
Notation ">^d%O" := dual_gt : function_scope.
Notation "<?=^d%O" := dual_leif : function_scope.
Notation "<?<=^d%O" := dual_lteif : function_scope.
Notation ">=<^d%O" := dual_comparable : function_scope.
Notation "><^d%O" := (fun x y ⇒ ~~ dual_comparable x y) : function_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 "\bot^d" := dual_bottom : order_scope.
Notation "\top^d" := dual_top : order_scope.

End DualSyntax.

Module DualPreorder.

Lemma leEdual (d : disp_t) (T : preorderType d) (x y : T) :
  (x <=^d y :> T ^d ) = (y ≤ x ).
Lemma ltEdual (d : disp_t) (T : preorderType d) (x y : T) :
  (x <^d y :> T ^d ) = (y < x ).

Lemma botEdual d (T : tPreorderType d) : (dual_bottom : T ^d ) = \top :> T.

Lemma topEdual d (T : bPreorderType d) : (dual_top : T ^d ) = \bot :> T.

End DualPreorder.

THEORY

Module Import PreorderTheory.
Section PreorderTheory.

Context {disp : disp_t} {T : preorderType disp}.

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

Definition nondecreasing disp' (T' : preorderType disp') (f : T → T') : Prop :=
  {homo f : x y / x ≤ y }.

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_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_le_def x y: (x < y ) = (x ≤ y ) && ~~ (y ≤ x ).

Lemma ltxx x: x < x = false.

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

Definition ltexx := (lexx , ltxx ).

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

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

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.

Lemma le_leP {x y} : reflect (∀ z, y ≤ z → x ≤ z) (x ≤ y).

Lemma le_geP {x y} : reflect (∀ z, z ≤ x → z ≤ y) (x ≤ y).

Lemma lt_ltP {x y} : reflect (∀ z, y ≤ z → x < z) (x < y).

Lemma lt_gtP {x y} : reflect (∀ z, z ≤ x → z < y) (x < y).

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_is_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 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 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_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 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 leif_refl x C : reflect (x ≤ x ?= iff C) 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 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.

min and max

monotonicity

Lemma comparable_bigl x x0 op I (P : pred I) F (s : seq I) :
  {in >=< x &, ∀ y z, op y z >=< x } → x0 >=< x →
  {in P , ∀ i, F i >=< x } → \big [op /x0 ]_(i <- s | P i ) F i >=< x.

Lemma comparable_bigr x x0 op I (P : pred I) F (s : seq I) :
  {in >=<%O x &, ∀ y z, x >=< op y z } → x >=< x0 →
  {in P , ∀ i, x >=< F i } → x >=< \big [op /x0 ]_(i <- s | P i ) F i.

Section bigminmax.

Variables (I : Type) (r : seq I) (f : I → T) (x0 x : T) (P : pred I).

Lemma bigmax_lt : x0 < x → (∀ i, P i → f i < x ) →
  \big [max /x0 ]_(i <- r | P i ) f i < x.

Lemma lt_bigmin : x < x0 → (∀ i, P i → x < f i ) →
  x < \big [min /x0 ]_(i <- r | P i ) f i.

End bigminmax.

End PreorderTheory.
#[global] Hint Resolve comparable_minr comparable_minl : core.
#[global] Hint Resolve comparable_maxr comparable_maxl : core.

Section ContraTheory.
Context {disp1 disp2 : disp_t} {T1 : preorderType disp1} {T2 : preorderType disp2}.
Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop).

Lemma comparable_contraTle b x y : x >=< y → (y < x → ~~ b ) → (b → x ≤ y ).

Lemma comparable_contraTlt b x y : x >=< y → (y ≤ x → ~~ b ) → (b → x < y ).

Lemma comparable_contraPle P x y : x >=< y → (y < x → ¬ P ) → (P → x ≤ y ).

Lemma comparable_contraPlt P x y : x >=< y → (y ≤ x → ¬ P ) → (P → x < y ).

Lemma comparable_contraNle b x y : x >=< y → (y < x → b ) → (~~ b → x ≤ y ).

Lemma comparable_contraNlt b x y : x >=< y → (y ≤ x → b ) → (~~ b → x < y ).

Lemma comparable_contra_not_le P x y : x >=< y → (y < x → P ) → (¬ P → x ≤ y ).

Lemma comparable_contra_not_lt P x y : x >=< y → (y ≤ x → P ) → (¬ P → x < y ).

Lemma comparable_contraFle b x y : x >=< y → (y < x → b ) → (b = false → x ≤ y ).

Lemma comparable_contraFlt b x y : x >=< y → (y ≤ x → b ) → (b = false → x < y ).

Lemma comparable_contra_leq_le m n x y : x >=< y →
  (y < x → (n < m)%N) → ((m ≤ n)%N → x ≤ y ).

Lemma comparable_contra_leq_lt m n x y : x >=< y →
  (y ≤ x → (n < m)%N) → ((m ≤ n)%N → x < y ).

Lemma comparable_contra_ltn_le m n x y : x >=< y →
  (y < x → (n ≤ m)%N) → ((m < n)%N → x ≤ y ).

Lemma comparable_contra_ltn_lt m n x y : x >=< y →
  (y ≤ x → (n ≤ m)%N) → ((m < n)%N → x < y ).

Lemma comparable_contra_le x y z t : z >=< t →
  (t < z → y < x ) → (x ≤ y → z ≤ t ).

Lemma comparable_contra_le_lt x y z t : z >=< t →
  (t ≤ z → y < x ) → (x ≤ y → z < t ).

Lemma comparable_contra_lt_le x y z t : z >=< t →
  (t < z → y ≤ x ) → (x < y → z ≤ t ).

Lemma comparable_contra_lt x y z t : z >=< t →
(t ≤ z → y ≤ x ) → (x < y → z < t ).

End ContraTheory.

Section PreorderMonotonyTheory.

Context {disp disp' : disp_t}.
Context {T : preorderType disp} {T' : preorderType disp'}.
Implicit Types (m n p : nat) (x y z : T) (u v w : T').
Variables (D D' : {pred T }) (f : T → T').

Hint Resolve lexx lt_le_def : core.

Lemma leW_mono : {mono f : x y / x ≤ y } → {mono f : x y / x < y }.

Lemma leW_nmono : {mono f : x y /~ x ≤ y } → {mono f : x y /~ x < y }.

Lemma leW_mono_in :
  {in D &, {mono f : x y / x ≤ y }} → {in D &, {mono f : x y / x < y }}.

Lemma leW_nmono_in :
  {in D &, {mono f : x y /~ x ≤ y }} → {in D &, {mono f : x y /~ x < y }}.

End PreorderMonotonyTheory.

End PreorderTheory.

#[global] Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core.

Arguments leif_refl {disp T x C}.

Module Import BPreorderTheory.
Section BPreorderTheory.
Context {disp : disp_t} {T : bPreorderType disp}.
Implicit Types (x y : T).

Lemma le0x x : \bot ≤ x.

Lemma ltx0 x : (x < \bot ) = false.

End BPreorderTheory.
End BPreorderTheory.

Module Import TPreorderTheory.
Section TPreorderTheory.
Context {disp : disp_t} {T : tPreorderType disp}.
Implicit Types (x y : T).

Lemma lex1 x : x ≤ \top.
Lemma lt1x x : (\top < x ) = false.

End TPreorderTheory.
End TPreorderTheory.

#[global] Hint Extern 0 (is_true (\bot ≤ _)) ⇒ exact: le0x : core.
#[global] Hint Extern 0 (is_true (_ ≤ \top)) ⇒ exact: lex1 : core.

FACTORIES preorder

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

Let ge_trans : transitive (fun x y ⇒ le y x).

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := @isDuallyPreorder.Build d T
le _ lt_def (fun x y ⇒ lt_def y x ) le_refl le_refl le_trans ge_trans.

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

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := @isPreorder.Build d T
  le _ (fun _ _ ⇒ erefl ) le_refl le_trans.

Let le_refl : reflexive le.

Let le_trans : transitive le.

Let lt_le_def x y : lt x y = (le x y ) && ~~ (le y x ).

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := @isPreorder.Build d T
  le lt lt_le_def le_refl le_trans .

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := @LtLe_isPreorder.Build d T
  _ lt (fun _ _ ⇒ erefl ) lt_irr lt_trans.

Module PreCancelPartial.
Section PreCancelPartial.
Variables (disp : disp_t) (T : choiceType).
Variables (disp' : disp_t) (T' : preorderType disp') (f : T → T').

Definition le (x y : T) := f x ≤ f y.
Definition lt (x y : T) := f x < f y.

Fact refl : reflexive le.
Fact trans : transitive le.
Fact ge_trans : transitive (fun x y ⇒ le y x).
Fact lt_le_def x y : lt x y = le x y && ~~ le y x.

Definition PrePcan := isPreorder.Build disp T lt_le_def refl trans.

End PreCancelPartial.
End PreCancelPartial.

FIXME Fail # [export] HB.instance Definition _ (disp : disp_t) (T : choiceType) (disp' : disp_t) (T' : porderType disp') (f : T -> T') (f_inj : injective f): isPreorder disp (inj_type f_inj) := @PreCancelPartial.PrePcan disp (inj_type f_inj) disp' T' f.

#[export ]
HB.instance Definition _ (disp : disp_t ) (T : Type )
  (disp' : disp_t ) (T' : preorderType disp') (f : T → T')
  (f' : T' → option T ) (f_can : pcancel f f') : isPreorder disp (pcan_type f_can ) :=
  @PreCancelPartial.PrePcan disp (pcan_type f_can ) disp' T' f.

#[export ]
HB.instance Definition _ (disp : disp_t ) (T : Type )
  (disp' : disp_t ) (T' : preorderType disp') (f : T → T')
  (f' : T' → T ) (f_can : cancel f f') : isPreorder disp (can_type f_can ) :=
  @PreCancelPartial.PrePcan disp (can_type f_can ) disp' T' f.

Morphism hierarchy.

Definition order_morphism d (T : preorderType d) d' (T' : preorderType d')
  (f : T → T') : Prop := {mono f : x y / x ≤ y }.

Module OrderMorphismExports.
Notation "{ 'omorphism' T -> T' }" :=
  (@OrderMorphism.type _ T%type _ T'%type) : type_scope.
End OrderMorphismExports.

Module Import OrderMorphismTheory.
Section OrderMorphismTheory.

Lemma omorph_le (d : disp_t) (T : preorderType d) (d' : disp_t) (T' : preorderType d')
(f : {omorphism T → T'}) : {homo f : x y / x ≤ y }.

Section IdCompFun.

Variables (d : disp_t) (T : preorderType d) (d' : disp_t) (T' : preorderType d').
Variables (d'' : disp_t) (T'' : preorderType d'').
Variables (f : {omorphism T' → T''}) (g : {omorphism T → T'}).

Fact idfun_is_nondecreasing : nondecreasing (@idfun T).
#[export ]
HB.instance Definition _ := isOrderMorphism.Build d T d T idfun
  idfun_is_nondecreasing.

Fact comp_is_nondecreasing : nondecreasing (f \o g).

#[export ]
HB.instance Definition _ := isOrderMorphism.Build d T d'' T'' (f \o g )
  comp_is_nondecreasing.

End IdCompFun.

End OrderMorphismTheory.
End OrderMorphismTheory.

#[short (type ="subPreorder")]
HB.structure Definition SubPreorder d (T : preorderType d ) S d' :=
  { U of SubEquality T S U & Preorder d' U & isSubPreorder d T S d' U }.

Module Import SubPreorderTheory.
Section SubPreorderTheory.
Context (d : disp_t) (T : preorderType d) (S : pred T).
Context (d' : disp_t) (U : SubPreorder.type S d').
Local Notation val := (val : U → T).
#[deprecated(since="mathcomp 2.3.0", note="Use le_val instead.")]
Lemma leEsub x y : (x ≤ y ) = (val x ≤ val y ).
Lemma lt_val : {mono val : x y / x < y }.
#[deprecated(since="mathcomp 2.3.0", note="Use lt_val instead.")]
Lemma ltEsub x y : (x < y ) = (val x < val y ).
Lemma le_wval : {homo val : x y / x ≤ y }.
Lemma lt_wval : {homo val : x y / x < y }.
End SubPreorderTheory.
Arguments lt_val {d T S d' U} x y.
Arguments le_wval {d T S d' U} x y.
Arguments lt_wval {d T S d' U} x y.
End SubPreorderTheory.

Fact valD : order_morphism (val : U → T).

Module SubOrderExports.

Notation "[ 'SubChoice_isSubPreorder' 'of' U 'by' <: ]" :=
  (SubChoice_isSubPreorder.Build _ _ _ _ U)
  (at level 0, format "[ 'SubChoice_isSubPreorder' 'of' U 'by' <: ]")
  : form_scope.
Notation "[ 'SubChoice_isSubPreorder' 'of' U 'by' <: 'with' disp ]" :=
  (SubChoice_isSubPreorder.Build _ _ _ disp U)
  (at level 0, format "[ 'SubChoice_isSubPreorder' 'of' U 'by' <: 'with' disp ]")
  : form_scope.

End SubOrderExports.

INSTANCES Instances on nat This is an example of creation of multiple instances on the same type, with distinct displays, using natural numbers. We declare two distinct canonical orders:

leq which is total, and where meet and join are minn and maxn, on nat
dvdn which is partial, and where meet and join are gcdn and lcmn, on natdvd

The Module NatOrder defines leq as the canonical order on the type nat, i.e., without creating an alias. We define and use nat_display and proceed like a standard canonical structure declaration, except that we use this display. We also use a single factory LeOrderMixin to instantiate three different canonical declarations porderType, distrLatticeType, orderType. We finish by providing theorems to convert the operations of ordered and lattice types to their definition without structure abstraction.

Module NatOrder.
Section NatOrder.

Fact nat_display : disp_t.

Lemma ltn_def x y : (x < y)%N = (x ≤ y)%N && ~~ (y ≤ x)%N.

#[export ]
HB.instance Definition _ :=
  isPreorder.Build nat_display nat ltn_def leqnn leq_trans.

#[export ]
HB.instance Definition _ := hasBottom.Build nat_display nat leq0n.

Lemma leEnat : le = leq.
Lemma ltEnat : lt = ltn.
Lemma minEnat : min = minn.
Lemma maxEnat : max = maxn.
Lemma botEnat : \bot = 0%N :> nat.

End NatOrder.

Module Exports.
Definition leEnat := leEnat.
Definition ltEnat := ltEnat.
Definition minEnat := minEnat.
Definition maxEnat := maxEnat.
Definition botEnat := botEnat.
End Exports.
End NatOrder.

Module NatMonotonyTheory.
Section NatMonotonyTheory.

Context {disp : disp_t} {T : preorderType disp}.
Variables (D : {pred nat }) (f : nat → T).
Hypothesis Dconvex : {in D &, ∀ i j k, i < k < j → k \in D }.

Lemma homo_ltn_lt_in : {in D , ∀ i, i .+1 \in D → f i < f i .+1 } →
  {in D &, {homo f : i j / i < j }}.

Lemma nondecn_inP : {in D , ∀ i, i .+1 \in D → f i ≤ f i .+1 } →
  {in D &, {homo f : i j / i ≤ j }}.

Lemma nhomo_ltn_lt_in : {in D , ∀ i, i .+1 \in D → f i > f i .+1 } →
  {in D &, {homo f : i j /~ i < j }}.

Lemma nonincn_inP : {in D , ∀ i, i .+1 \in D → f i ≥ f i .+1 } →
  {in D &, {homo f : i j /~ i ≤ j }}.

Lemma homo_ltn_lt : (∀ i, f i < f i .+1 ) → {homo f : i j / i < j }.

Lemma nondecnP : (∀ i, f i ≤ f i .+1 ) → {homo f : i j / i ≤ j }.

Lemma nhomo_ltn_lt : (∀ i, f i > f i .+1 ) → {homo f : i j /~ i < j }.

Lemma nonincnP : (∀ i, f i ≥ f i .+1 ) → {homo f : i j /~ i ≤ j }.

End NatMonotonyTheory.
Arguments homo_ltn_lt_in {disp T} [D f].
Arguments nondecn_inP {disp T} [D f].
Arguments nhomo_ltn_lt_in {disp T} [D f].
Arguments nonincn_inP {disp T} [D f].
Arguments homo_ltn_lt {disp T} [f].
Arguments nondecnP {disp T} [f].
Arguments nhomo_ltn_lt {disp T} [f].
Arguments nonincnP {disp T} [f].
End NatMonotonyTheory.

The Module DvdSyntax introduces a new set of notations using the newly created display dvd_display. We first define the display as an opaque definition of type disp_t, and we use it as the first argument of the operator which display we want to change from the default one (here le, lt, dvd sdvd, meet, join, top and bottom, as well as big op notations on gcd and lcm). This notations will now be used for any ordered type which first parameter is set to dvd_display.

Fact dvd_display : disp_t.

Module DvdSyntax.

Notation dvd := (@le dvd_display _).
Notation "@ 'dvd' T" := (@le dvd_display T)
(at level 10, T at level 8, only parsing) : function_scope.
Notation sdvd := (@lt dvd_display _).
Notation "@ 'sdvd' T" := (@lt dvd_display T)
(at level 10, T at level 8, only parsing) : function_scope.

Notation "x %| y" := (dvd x y) : order_scope.
Notation "x %<| y" := (sdvd x y) : order_scope.

Notation nat0 := (@top dvd_display _).
Notation nat1 := (@bottom dvd_display _).

End DvdSyntax.

The Module NatDvd defines dvdn as the canonical order on NatDvd.t, which is abbreviated using the notation natdvd at the end of the module. We use the newly defined dvd_display, described above. We first recover structures that are common to both nat and natdvd (eqType, choiceType, countType) through the copy mechanism, then we use a single factory MeetJoinMixin to instantiate both porderType and distrLatticeType canonical structures, and end with top and bottom. We finish by providing theorems to convert the operations of ordered and lattice types to their definition without structure abstraction.

Module NatDvd.
Section NatDvd.
Implicit Types (m n p : nat).

Definition t := nat.

#[export ]
HB.instance Definition _ := Choice.copy t nat.

Note that this where the dvd_display is associated with the type NatDvd.t.

#[export ]
HB.instance Definition _ := @Le_isPreorder.Build
dvd_display t dvdn dvdnn dvdn_trans.

NatDvd.t is associated below with the notation "natdvd".

#[export ]
HB.instance Definition _ := @hasBottom.Build _ t 1 dvd1n.

#[export ]
HB.instance Definition _ := @hasTop.Build _ t 0 dvdn0.

Import DvdSyntax.
Lemma dvdE : dvd = dvdn :> rel t.
Lemma nat1E : nat1 = 1%N :> t.
Lemma nat0E : nat0 = 0%N :> t.

End NatDvd.
Module Exports.
Notation natdvd := t.
Definition dvdEnat := dvdE.
Definition nat1E := nat1E.
Definition nat0E := nat0E.
End Exports.
End NatDvd.

Instances on ordinal

Module OrdinalOrder.
Section OrdinalOrder.

Fact ord_display : disp_t.

Section PossiblyTrivial.
Context (n : nat).

#[export ]
HB.instance Definition _ :=
[SubChoice_isSubPreorder of 'I_n by <: with ord_display ].

Lemma leEord : (le : rel 'I_n ) = leq.
Lemma ltEord : (lt : rel 'I_n ) = (fun m n ⇒ m < n)%N.
End PossiblyTrivial.

Section NonTrivial.
Context (n' : nat).
Let n := n'.+1.

#[export ] HB.instance Definition _ := @hasBottom.Build _ 'I_n ord0 leq0n.
#[export ] HB.instance Definition _ := @hasTop.Build _ 'I_n ord_max (@leq_ord _).

Lemma botEord : \bot = ord0.
Lemma topEord : \top = ord_max.

End NonTrivial.

End OrdinalOrder.

Module Exports.
Definition leEord := leEord.
Definition ltEord := ltEord.
Definition botEord := botEord.
Definition topEord := topEord.
End Exports.
End OrdinalOrder.

Instances on bool

Module BoolOrder.
Section BoolOrder.
Implicit Types (x y : bool).

Fact bool_display : disp_t.

Fact ltn_def x y : (x < y)%N = (x ≤ y)%N && ~~ (y ≤ x)%N.

#[export ] HB.instance Definition _ := @isPreorder.Build bool_display bool
_ _ ltn_def leqnn leq_trans.
#[export ] HB.instance Definition _ := @hasBottom.Build _ bool false leq0n.
#[export ] HB.instance Definition _ := @hasTop.Build _ bool true leq_b1.

Lemma leEbool : le = (leq : rel bool ).
Lemma ltEbool x y : (x < y ) = (x < y)%N.

End BoolOrder.
Module Exports.
Definition leEbool := leEbool.
Definition ltEbool := ltEbool.
End Exports.
End BoolOrder.

Definition of prod_display

Fact prod_display_unit (_ _ : unit) : unit.

Definition prod_display (displ dispr : disp_t) : disp_t :=
  Disp (prod_display_unit (d1 displ) (d1 dispr))
       (prod_display_unit (d2 displ) (d2 dispr)).

Fact seqprod_display (disp : disp_t) : disp_t.

Module Import ProdSyntax.

Notation "<=^p%O" := (@le (prod_display _ _) _) : function_scope.
Notation ">=^p%O" := (@ge (prod_display _ _) _) : function_scope.
Notation ">=^p%O" := (@ge (prod_display _ _) _) : function_scope.
Notation "<^p%O" := (@lt (prod_display _ _) _) : function_scope.
Notation ">^p%O" := (@gt (prod_display _ _) _) : function_scope.
Notation "<?=^p%O" := (@leif (prod_display _ _) _) : function_scope.
Notation ">=<^p%O" := (@comparable (prod_display _ _) _) : function_scope.
Notation "><^p%O" := (fun x y ⇒ ~~ (@comparable (prod_display _ _) _ x y )) :
  function_scope.

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

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

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

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

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

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

Notation ">=<^p y" := [pred x | >=<^p %O x y ] : order_scope.
Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope.
Notation "x >=<^p y" := (>=<^p %O x y) : order_scope.

Notation "><^p y" := [pred x | ~~ (>=<^p %O x y )] : order_scope.
Notation "><^p y :> T" := (><^p (y : T)) (only parsing) : order_scope.
Notation "x ><^p y" := (~~ (><^p %O x y )) : order_scope.

End ProdSyntax.

Module Import SeqProdSyntax.

Notation "<=^sp%O" := (@le (seqprod_display _) _) : function_scope.
Notation ">=^sp%O" := (@ge (seqprod_display _) _) : function_scope.
Notation ">=^sp%O" := (@ge (seqprod_display _) _) : function_scope.
Notation "<^sp%O" := (@lt (seqprod_display _) _) : function_scope.
Notation ">^sp%O" := (@gt (seqprod_display _) _) : function_scope.
Notation "<?=^sp%O" := (@leif (seqprod_display _) _) : function_scope.
Notation ">=<^sp%O" := (@comparable (seqprod_display _) _) : function_scope.
Notation "><^sp%O" := (fun x y ⇒ ~~ (@comparable (seqprod_display _) _ x y )) :
  function_scope.

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

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

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

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

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

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

Notation ">=<^sp y" := [pred x | >=<^sp %O x y ] : order_scope.
Notation ">=<^sp y :> T" := (>=<^sp (y : T)) (only parsing) : order_scope.
Notation "x >=<^sp y" := (>=<^sp %O x y) : order_scope.

Notation "><^sp y" := [pred x | ~~ (>=<^sp %O x y )] : order_scope.
Notation "><^sp y :> T" := (><^sp (y : T)) (only parsing) : order_scope.
Notation "x ><^sp y" := (~~ (><^sp %O x y )) : order_scope.

End SeqProdSyntax.

Definition of lexi_display

Fact lexi_display (disp _ : disp_t) : disp_t.

Fact seqlexi_display (disp : disp_t) : disp_t.

Module Import LexiSyntax.

Notation "<=^l%O" := (@le (lexi_display _ _) _) : function_scope.
Notation ">=^l%O" := (@ge (lexi_display _ _) _) : function_scope.
Notation ">=^l%O" := (@ge (lexi_display _ _) _) : function_scope.
Notation "<^l%O" := (@lt (lexi_display _ _) _) : function_scope.
Notation ">^l%O" := (@gt (lexi_display _ _) _) : function_scope.
Notation "<?=^l%O" := (@leif (lexi_display _ _) _) : function_scope.
Notation ">=<^l%O" := (@comparable (lexi_display _ _) _) : function_scope.
Notation "><^l%O" := (fun x y ⇒ ~~ (@comparable (lexi_display _ _) _ x y )) :
  function_scope.

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

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

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

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

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

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

Notation ">=<^l y" := [pred x | >=<^l %O x y ] : order_scope.
Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope.
Notation "x >=<^l y" := (>=<^l %O x y) : order_scope.

Notation "><^l y" := [pred x | ~~ (>=<^l %O x y )] : order_scope.
Notation "><^l y :> T" := (><^l (y : T)) (only parsing) : order_scope.
Notation "x ><^l y" := (~~ (><^l %O x y )) : order_scope.

End LexiSyntax.

Module Import SeqLexiSyntax.

Notation "<=^l%O" := (@le (seqlexi_display _ _) _) : function_scope.
Notation ">=^l%O" := (@ge (seqlexi_display _ _) _) : function_scope.
Notation ">=^l%O" := (@ge (seqlexi_display _ _) _) : function_scope.
Notation "<^l%O" := (@lt (seqlexi_display _ _) _) : function_scope.
Notation ">^l%O" := (@gt (seqlexi_display _ _) _) : function_scope.
Notation "<?=^l%O" := (@leif (seqlexi_display _ _) _) : function_scope.
Notation ">=<^l%O" := (@comparable (seqlexi_display _ _) _) : function_scope.
Notation "><^l%O" := (fun x y ⇒ ~~ (@comparable (seqlexi_display _ _) _ x y )) :
  function_scope.

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

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

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

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

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

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

Notation ">=<^l y" := [pred x | >=<^l %O x y ] : order_scope.
Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope.
Notation "x >=<^l y" := (>=<^l %O x y) : order_scope.

Notation "><^l y" := [pred x | ~~ (>=<^l %O x y )] : order_scope.
Notation "><^l y :> T" := (><^l (y : T)) (only parsing) : order_scope.
Notation "x ><^l y" := (~~ (><^l %O x y )) : order_scope.

End SeqLexiSyntax.

We declare an alias of the cartesian product which has canonical product order.

Module ProdOrder.

Local Open Scope type_scope. (* FIXME *)

Definition type (disp : disp_t) (T T' : Type) := T × T'.
Definition type_
  (disp1 disp2 : disp_t) (T : preorderType disp1) (T' : preorderType disp2) :=
  type (prod_display disp1 disp2) T T'.

Section Basis.
Context {disp : disp_t}.

Local Notation "T * T'" := (type disp T T') : type_scope.

#[export ] HB.instance Definition _ (T T' : eqType ) := Equality.on (T × T').
#[export ] HB.instance Definition _ (T T' : choiceType ) := Choice.on (T × T').
#[export ] HB.instance Definition _ (T T' : countType ) := Countable.on (T × T').
#[export ] HB.instance Definition _ (T T' : finType ) := Finite.on (T × T').

End Basis.

Section Preorder.
Context (disp1 disp2 : disp_t).
Context (T1 : preorderType disp1) (T2 : preorderType disp2).
Implicit Types (x y : T1 × T2).

Let le x y := (x .1 ≤ y .1 ) && (x .2 ≤ y .2 ).

Let lt x y := (x .1 < y .1 ) && (x .2 ≤ y .2 ) || (x .1 ≤ y .1 ) && (x .2 < y .2 ).

Fact lt_def x y : lt x y = le x y && ~~ le y x.

Fact refl : reflexive le.

Fact trans : transitive le.

End Preorder.

Section Preorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : preorderType disp1) (T2 : preorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.
Implicit Types (x y : T1 × T2).

Let T1' : Type := T1.
Let T2' : Type := T2.

Definition le x y := (x .1 ≤ y .1 ) && (x .2 ≤ y .2 ).

Definition lt x y := (x .1 < y .1 ) && (x .2 ≤ y .2 ) || (x .1 ≤ y .1 ) && (x .2 < y .2 ).

#[export ]
HB.instance Definition _ := @isDuallyPreorder.Build disp3 (T1 × T2 ) le lt
  (@lt_def _ _ T1' T2') (@lt_def _ _ T1 ^d T2 ^d )
  (@refl _ _ T1' T2') (@refl _ _ T1 ^d T2 ^d )
  (@trans _ _ T1' T2') (@trans _ _ T1 ^d T2 ^d ).

Lemma leEprod x y : (x ≤ y ) = (x .1 ≤ y .1 ) && (x .2 ≤ y .2 ).

Lemma ltEprod x y :
  (x < y ) = (x .1 < y .1 ) && (x .2 ≤ y .2 ) || (x .1 ≤ y .1 ) && (x .2 < y .2 ).

Lemma le_pair (x1 y1 : T1) (x2 y2 : T2) :
  (x1 , x2 ) ≤ (y1 , y2 ) :> T1 × T2 = (x1 ≤ y1 ) && (x2 ≤ y2 ).

Lemma lt_pair (x1 y1 : T1) (x2 y2 : T2) :
  (x1 , x2 ) < (y1 , y2 ) :> T1 × T2
  = (x1 < y1 ) && (x2 ≤ y2 ) || (x1 ≤ y1 ) && (x2 < y2 ).

End Preorder.

Section BPreorder.
Context (disp1 disp2 : disp_t).
Context (T1 : bPreorderType disp1) (T2 : bPreorderType disp2).
Local Notation "T1 * T2" := (type (Disp tt tt) T1 T2) : type_scope.
Implicit Types (x : T1 × T2).

Fact le0x x : (\bot , \bot ) ≤ x :> T1 × T2.

End BPreorder.

Section BPreorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : bPreorderType disp1) (T2 : bPreorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.

Let T1' : Type := T1.
Let T2' : Type := T2.

#[export ]
HB.instance Definition _ :=
  @hasBottom.Build disp3 (T1 × T2 ) (\bot , \bot ) (@le0x _ _ T1' T2').

Lemma botEprod : \bot = (\bot , \bot ) :> T1 × T2.

End BPreorder.

Section TPreorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : tPreorderType disp1) (T2 : tPreorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.

#[export ]
HB.instance Definition _ :=
  @hasTop.Build disp3 (T1 × T2 ) (\top , \top ) (@le0x _ _ T1 ^d T2 ^d ).

Lemma topEprod : \top = (\top , \top ) :> T1 × T2.

End TPreorder.

FIXME: use HB.saturate

#[export ]
HB.instance Definition _ (disp1 disp2 disp3 : disp_t )
(T1 : tbPreorderType disp1 ) (T2 : tbPreorderType disp2 ) :=
Preorder.on (type disp3 T1 T2 ).

FIXME: use HB.saturate

Section FinPreorder.
Context (disp1 disp2 disp3 : disp_t).

#[export ]
HB.instance Definition _ (T1 : finPreorderType disp1 )
  (T2 : finPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finBPreorderType disp1 )
  (T2 : finBPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finTPreorderType disp1 )
  (T2 : finTPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finTBPreorderType disp1 )
  (T2 : finTBPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).

End FinPreorder.

Module Exports.
Notation "T *prod[ d ] T'" := (type d T T')
  (at level 70, d at next level, format "T *prod[ d ] T'") : type_scope.
Notation "T *p T'" := (type_ T T')
  (at level 70, format "T *p T'") : type_scope.
Definition leEprod := @leEprod.
Definition ltEprod := @ltEprod.
Definition le_pair := @le_pair.
Definition lt_pair := @lt_pair.
Definition botEprod := @botEprod.
Definition topEprod := @topEprod.
End Exports.
End ProdOrder.

Module DefaultProdOrder.
Section DefaultProdOrder.
Context {disp1 disp2 : disp_t}.

Let prod T1 T2 := T1 ×prod [prod_display disp1 disp2 ] T2.

FIXME: Scopes of arguments are broken in several places. FIXME: Declaring a bunch of copies is still a bit painful.

End DefaultProdOrder.
End DefaultProdOrder.

We declare an alias of the cartesian product, which has canonical lexicographic order.

Module ProdLexiOrder.

Local Open Scope type_scope. (* FIXME *)

Definition type (disp : disp_t) (T T' : Type) := T × T'.
Definition type_
  (disp1 disp2 : disp_t) (T : preorderType disp1) (T' : preorderType disp2) :=
  type (lexi_display disp1 disp2) T T'.

Section Basis.
Context {disp : disp_t}.

Local Notation "T * T'" := (type disp T T') : type_scope.

#[export ] HB.instance Definition _ (T T' : eqType ) := Equality.on (T × T').
#[export ] HB.instance Definition _ (T T' : choiceType ) := Choice.on (T × T').
#[export ] HB.instance Definition _ (T T' : countType ) := Countable.on (T × T').
#[export ] HB.instance Definition _ (T T' : finType ) := Finite.on (T × T').

End Basis.

Section Preorder.
Context (disp1 disp2 : disp_t).
Context (T1 : preorderType disp1) (T2 : preorderType disp2).
Implicit Types (x y : T1 × T2).

Let le x y := (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 ≤ y .2 )).
Let lt x y := (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 < y .2 )).

Fact refl : reflexive le.

Fact trans : transitive le.

Fact lt_le_def x y : lt x y = le x y && ~~ le y x.

End Preorder.

Section Preorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : preorderType disp1) (T2 : preorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.
Implicit Types (x y : T1 × T2).

Let T1' : Type := T1.
Let T2' : Type := T2.

Definition le x y := (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 ≤ y .2 )).
Definition lt x y := (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 < y .2 )).

#[export ]
HB.instance Definition _ := @isDuallyPreorder.Build disp3 (T1 × T2 ) le lt
  (@lt_le_def _ _ T1' T2') (@lt_le_def _ _ T1 ^d T2 ^d )
  (@refl _ _ T1' T2') (@refl _ _ T1 ^d T2 ^d )
  (@trans _ _ T1' T2') (@trans _ _ T1 ^d T2 ^d ).

Lemma leEprodlexi x y :
  (x ≤ y ) = (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 ≤ y .2 )).

Lemma ltEprodlexi x y :
  (x < y ) = (x .1 ≤ y .1 ) && ((x .1 ≥ y .1 ) ==> (x .2 < y .2 )).

Lemma lexi_pair (x1 y1 : T1) (x2 y2 : T2) :
   (x1 , x2 ) ≤ (y1 , y2 ) :> T1 × T2 = (x1 ≤ y1 ) && ((x1 ≥ y1 ) ==> (x2 ≤ y2 )).

Lemma ltxi_pair (x1 y1 : T1) (x2 y2 : T2) :
   (x1 , x2 ) < (y1 , y2 ) :> T1 × T2 = (x1 ≤ y1 ) && ((x1 ≥ y1 ) ==> (x2 < y2 )).

End Preorder.

Section BPreorder.
Context (disp1 disp2 : disp_t).
Context (T1 : bPreorderType disp1) (T2 : bPreorderType disp2).
Local Notation "T1 * T2" := (type (Disp tt tt) T1 T2) : type_scope.
Implicit Types (x : T1 × T2).

Fact le0x x : (\bot , \bot ) ≤ x :> T1 × T2.

End BPreorder.

Section BPreorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : bPreorderType disp1) (T2 : bPreorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.

Let T1' : Type := T1.
Let T2' : Type := T2.

#[export ]
HB.instance Definition _ :=
  @hasBottom.Build disp3 (T1 × T2 ) (\bot , \bot ) (@le0x _ _ T1' T2').

Lemma botEprodlexi : \bot = (\bot , \bot ) :> T1 × T2.

End BPreorder.

Section TPreorder.
Context (disp1 disp2 disp3 : disp_t).
Context (T1 : tPreorderType disp1) (T2 : tPreorderType disp2).
Local Notation "T1 * T2" := (type disp3 T1 T2) : type_scope.

#[export ]
HB.instance Definition _ :=
  @hasTop.Build disp3 (T1 × T2 ) (\top , \top ) (@le0x _ _ T1 ^d T2 ^d ).

Lemma topEprodlexi : \top = (\top , \top ) :> T1 × T2.

End TPreorder.

FIXME: use HB.saturate

#[export ]
HB.instance Definition _ (disp1 disp2 disp3 : disp_t )
  (T1 : tbPreorderType disp1 ) (T2 : tbPreorderType disp2 ) :=
  Preorder.on (type disp3 T1 T2 ).

Lemma sub_prod_lexi (disp1 disp2 disp3 disp4 : disp_t)
  (T1 : preorderType disp1) (T2 : preorderType disp2) :
  subrel (<=%O : rel (T1 ×prod [disp3 ] T2)) (<=%O : rel (type disp4 T1 T2)).

FIXME: use HB.saturate

Section ProdLexiOrder.
Context (disp1 disp2 disp3 : disp_t).

#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (T1 : bPreorderType disp1 )
  (T2 : bPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (T1 : tPreorderType disp1 )
  (T2 : tPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (T1 : tbPreorderType disp1 )
  (T2 : tbPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finPreorderType disp1 )
  (T2 : finPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finBPreorderType disp1 )
  (T2 : finBPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finTPreorderType disp1 )
  (T2 : finTPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).
#[export ]
HB.instance Definition _ (T1 : finTBPreorderType disp1 )
  (T2 : finTBPreorderType disp2 ) := Preorder.on (type disp3 T1 T2 ).

End ProdLexiOrder.

Module Exports.

Notation "T *lexi[ d ] T'" := (type d T T')
  (at level 70, d at next level, format "T *lexi[ d ] T'") : type_scope.
Notation "T *l T'" := (type_ T T')
  (at level 70, format "T *l T'") : type_scope.

Definition leEprodlexi := @leEprodlexi.
Definition ltEprodlexi := @ltEprodlexi.
Definition lexi_pair := @lexi_pair.
Definition ltxi_pair := @ltxi_pair.
Definition topEprodlexi := @topEprodlexi.
Definition botEprodlexi := @botEprodlexi.
Definition sub_prod_lexi := @sub_prod_lexi.

End Exports.
End ProdLexiOrder.

Module DefaultProdLexiOrder.
Section DefaultProdLexiOrder.
Context {disp1 disp2 : disp_t}.

Let prodlexi T1 T2 := T1 ×lexi [lexi_display disp1 disp2 ] T2.

FIXME: Scopes of arguments are broken in several places. FIXME: Declaring a bunch of copies is still a bit painful.

End DefaultProdLexiOrder.
End DefaultProdLexiOrder.

We declare an alias of the sequences, which has canonical product order.

Module SeqProdOrder.
Section SeqProdOrder.

Definition type (disp : disp_t) T := seq T.
Definition type_ (disp : disp_t) (T : preorderType disp) :=
  type (seqprod_display disp) T.

Context {disp disp' : disp_t}.

Local Notation seq := (type disp').

#[export ] HB.instance Definition _ (T : eqType ) := Equality.on (seq T ).
#[export ] HB.instance Definition _ (T : choiceType ) := Choice.on (seq T ).
#[export ] HB.instance Definition _ (T : countType ) := Countable.on (seq T ).

Section Preorder.
Context (T : preorderType disp).
Implicit Types (s : seq T).

Fixpoint le s1 s2 := if s1 isn't x1 :: s1' then true else
                     if s2 isn't x2 :: s2' then false else
                     (x1 ≤ x2) && le s1' s2'.

Fact refl : reflexive le.

Fact trans : transitive le.

#[export ]
HB.instance Definition _ := isPreorder.Build disp' (seq T ) (rrefl _) refl trans.

Lemma leEseq s1 s2 : s1 ≤ s2 = if s1 isn't x1 :: s1' then true else
                                if s2 isn't x2 :: s2' then false else
                                (x1 ≤ x2) && (s1' ≤ s2' :> seq _).

Lemma le0s s : [::] ≤ s :> seq _.

Lemma les0 s : s ≤ [::] = (s == [::]).

Lemma le_cons x1 s1 x2 s2 :
   x1 :: s1 ≤ x2 :: s2 :> seq _ = (x1 ≤ x2 ) && (s1 ≤ s2 ).

#[export ]
HB.instance Definition _ := hasBottom.Build _ (seq T ) le0s.

Lemma botEseq : \bot = [::] :> seq T.
End Preorder.

End SeqProdOrder.

Module Exports.

Notation seqprod_with := type.
Notation seqprod := type_.

Definition leEseq := @leEseq.
Definition le0s := @le0s.
Definition les0 := @les0.
Definition le_cons := @le_cons.
Definition botEseq := @botEseq.

End Exports.
End SeqProdOrder.

Module DefaultSeqProdOrder.
Section DefaultSeqProdOrder.
Context {disp : disp_t}.

Notation seqprod := (seqprod_with (seqprod_display disp)).

End DefaultSeqProdOrder.
End DefaultSeqProdOrder.

We declare an alias of the sequences, which has canonical lexicographic order.

Module SeqLexiOrder.
Section SeqLexiOrder.

Definition type (disp : disp_t) T := seq T.
Definition type_ (disp : disp_t) (T : preorderType disp) :=
  type (seqlexi_display disp) T.

Context {disp disp' : disp_t}.

Local Notation seq := (type disp').

#[export ] HB.instance Definition _ (T : eqType ) := Equality.on (seq T ).
#[export ] HB.instance Definition _ (T : choiceType ) := Choice.on (seq T ).
#[export ] HB.instance Definition _ (T : countType ) := Countable.on (seq T ).

Section Preorder.
Context (T : preorderType disp).
Implicit Types (s : seq T).

Fixpoint le s1 s2 := if s1 isn't x1 :: s1' then true else
                     if s2 isn't x2 :: s2' then false else
                       (x1 ≤ x2) && ((x1 ≥ x2) ==> le s1' s2').
Fixpoint lt s1 s2 := if s2 isn't x2 :: s2' then false else
                     if s1 isn't x1 :: s1' then true else
                       (x1 ≤ x2) && ((x1 ≥ x2) ==> lt s1' s2').

Fact refl: reflexive le.

Fact trans: transitive le.

Lemma lt_le_def s1 s2 : lt s1 s2 = le s1 s2 && ~~ le s2 s1.

#[export ]
HB.instance Definition _ := isPreorder.Build disp' (seq T ) lt_le_def refl trans.

Lemma leEseqlexi s1 s2 :
   s1 ≤ s2 = if s1 isn't x1 :: s1' then true else
              if s2 isn't x2 :: s2' then false else
              (x1 ≤ x2) && ((x1 ≥ x2) ==> (s1' ≤ s2' :> seq T )).

Lemma ltEseqlexi s1 s2 :
   s1 < s2 = if s2 isn't x2 :: s2' then false else
              if s1 isn't x1 :: s1' then true else
              (x1 ≤ x2) && ((x1 ≥ x2) ==> (s1' < s2' :> seq T )).

Lemma lexi0s s : [::] ≤ s :> seq T.

Lemma lexis0 s : s ≤ [::] = (s == [::]).

Lemma ltxi0s s : ([::] < s :> seq T ) = (s != [::]).

Lemma ltxis0 s : s < [::] = false.

Lemma lexi_cons x1 s1 x2 s2 :
  x1 :: s1 ≤ x2 :: s2 :> seq T = (x1 ≤ x2 ) && ((x1 ≥ x2 ) ==> (s1 ≤ s2 )).

Lemma ltxi_cons x1 s1 x2 s2 :
  x1 :: s1 < x2 :: s2 :> seq T = (x1 ≤ x2 ) && ((x1 ≥ x2 ) ==> (s1 < s2 )).

Lemma lexi_lehead x s1 y s2 : x :: s1 ≤ y :: s2 :> seq T → x ≤ y.

Lemma ltxi_lehead x s1 y s2 : x :: s1 < y :: s2 :> seq T → x ≤ y.

Lemma eqhead_lexiE (x : T) s1 s2 : (x :: s1 ≤ x :: s2 :> seq _) = (s1 ≤ s2 ).

Lemma eqhead_ltxiE (x : T) s1 s2 : (x :: s1 < x :: s2 :> seq _) = (s1 < s2 ).

#[export ]
HB.instance Definition _ := hasBottom.Build _ (seq T ) lexi0s.

End Preorder.

Lemma sub_seqprod_lexi d (T : preorderType disp) :
   subrel (<=%O : rel (seqprod_with d T)) (<=%O : rel (seq T)).

End SeqLexiOrder.

Module Exports.

Notation seqlexi_with := type.
Notation seqlexi := type_.

Definition leEseqlexi := @leEseqlexi.
Definition lexi0s := @lexi0s.
Definition lexis0 := @lexis0.
Definition lexi_cons := @lexi_cons.
Definition lexi_lehead := @lexi_lehead.
Definition eqhead_lexiE := @eqhead_lexiE.

Definition ltEseqltxi := @ltEseqlexi.
Definition ltxi0s := @ltxi0s.
Definition ltxis0 := @ltxis0.
Definition ltxi_cons := @ltxi_cons.
Definition ltxi_lehead := @ltxi_lehead.
Definition eqhead_ltxiE := @eqhead_ltxiE.
Definition sub_seqprod_lexi := @sub_seqprod_lexi.

End Exports.
End SeqLexiOrder.

Module DefaultSeqLexiOrder.
Section DefaultSeqLexiOrder.
Context {disp : disp_t}.

Notation seqlexi := (seqlexi_with (seqlexi_display disp)).

End DefaultSeqLexiOrder.
End DefaultSeqLexiOrder.

We declare an alias of the tuples, which has canonical product order.

Module TupleProdOrder.
Import DefaultSeqProdOrder.

Section TupleProdOrder.

Definition type (disp : disp_t) n T := n .-tuple T.
Definition type_ (disp : disp_t) n (T : preorderType disp) :=
  type (seqprod_display disp) n T.

Context {disp disp' : disp_t}.
Local Notation "n .-tuple" := (type disp' n) : type_scope.

Section Basics.
Context (n : nat).
#[export ] HB.instance Definition _ (T : eqType ) := Equality.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : eqType ) := SubEquality.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : choiceType ) :=
  SubChoice.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : countType ) :=
  SubCountable.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : finType ) := SubFinite.on (n .-tuple T ).
End Basics.

Section Preorder.
Implicit Types (n : nat) (T : preorderType disp).

FIXME: this instance should be dualizable, but then we should not depend on the subtype mechanism, because the pointwise order on seq cannot be the dual of itself.

#[export ] HB.instance Definition _ n T :=
  [SubChoice_isSubPreorder of n .-tuple T by <: with disp'].

Lemma leEtprod n T (t1 t2 : n .-tuple T) :
   t1 ≤ t2 = [∀ i , tnth t1 i ≤ tnth t2 i ].

Lemma ltEtprod n T (t1 t2 : n .-tuple T) :
  t1 < t2 = [∃ i , tnth t1 i < tnth t2 i ] &&
            [∀ i , tnth t1 i ≤ tnth t2 i ].

End Preorder.

Section BPreorder.
Context (n : nat) (T : bPreorderType disp).
Implicit Types (t : n .-tuple T).

Fact le0x t : [tuple \bot | _ < n ] ≤ t :> n .-tuple T.

#[export ]
HB.instance Definition _ := hasBottom.Build _ (n .-tuple T ) le0x.

Lemma botEtprod : \bot = [tuple \bot | _ < n ] :> n .-tuple T.

End BPreorder.

Section TPreorder.
Context (n : nat) (T : tPreorderType disp).
Implicit Types (t : n .-tuple T).

Fact lex1 t : t ≤ [tuple \top | _ < n ] :> n .-tuple T.

#[export ]
HB.instance Definition _ := hasTop.Build _ (n .-tuple T ) lex1.

Lemma topEtprod : \top = [tuple \top | _ < n ] :> n .-tuple T.

End TPreorder.

FIXME: use HB.saturate

#[export ]
HB.instance Definition _ (n : nat ) (T : tbPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export ]
HB.instance Definition _ (n : nat ) (T : finPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (n : nat ) (T : finPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export ]
HB.instance Definition _ (n : nat ) (T : finBPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export ]
HB.instance Definition _ (n : nat ) (T : finTPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export ]
HB.instance Definition _ (n : nat ) (T : finTBPreorderType disp ) :=
  Preorder.on (n .-tuple T ).

End TupleProdOrder.

Module Exports.

Notation "n .-tupleprod[ disp ]" := (type disp n)
  (format "n .-tupleprod[ disp ]") : type_scope.
Notation "n .-tupleprod" := (type_ n)
  (format "n .-tupleprod") : type_scope.

Definition leEtprod := @leEtprod.
Definition ltEtprod := @ltEtprod.
Definition botEtprod := @botEtprod.
Definition topEtprod := @topEtprod.

End Exports.
End TupleProdOrder.

Module DefaultTupleProdOrder.
Section DefaultTupleProdOrder.
Context {disp : disp_t}.

Notation "n .-tupleprod" := n.-tupleprod [seqprod_display disp ].

End DefaultTupleProdOrder.
End DefaultTupleProdOrder.

We declare an alias of the tuples, which has canonical lexicographic order.

Module TupleLexiOrder.
Section TupleLexiOrder.
Import DefaultSeqLexiOrder.

Definition type (disp : disp_t) n T := n .-tuple T.
Definition type_ (disp : disp_t) n (T : preorderType disp) :=
  type (seqlexi_display disp) n T.

Context {disp disp' : disp_t}.
Local Notation "n .-tuple" := (type disp' n) : type_scope.

Section Basics.
Context (n : nat).
#[export ] HB.instance Definition _ (T : eqType ) := Equality.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : choiceType ) :=
  SubChoice.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : countType ) :=
  SubCountable.on (n .-tuple T ).
#[export ] HB.instance Definition _ (T : finType ) :=
  SubFinite.on (n .-tuple T ).
End Basics.

Section Preorder.
Implicit Types (T : preorderType disp).

#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ n T := SubChoice.on (n .-tuple T ).
#[export ]
HB.instance Definition _ n T :=
  [SubChoice_isSubPreorder of n .-tuple T by <: with disp'].

End Preorder.

Section BPreorder.
Context (n : nat) (T : bPreorderType disp).
Implicit Types (t : n .-tuple T).

Fact le0x t : [tuple \bot | _ < n ] ≤ t :> n .-tuple T.

#[export ] HB.instance Definition _ := hasBottom.Build _ (n .-tuple T ) le0x.

Lemma botEtlexi : \bot = [tuple \bot | _ < n ] :> n .-tuple T.

End BPreorder.

Section TPreorder.
Context (n : nat) (T : tPreorderType disp).
Implicit Types (t : n .-tuple T).

Fact lex1 t : t ≤ [tuple \top | _ < n ].

#[export ] HB.instance Definition _ := hasTop.Build _ (n .-tuple T ) lex1.

Lemma topEtlexi : \top = [tuple \top | _ < n ] :> n .-tuple T.

End TPreorder.

FIXME: use HB.saturate

#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (n : nat ) (T : bPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export , warning ="-HB.no-new-instance"]
HB.instance Definition _ (n : nat ) (T : tPreorderType disp ) :=
  Preorder.on (n .-tuple T ).
#[export ]
HB.instance Definition _ (n : nat ) (T : tbPreorderType disp ) :=
  Preorder.on (n .-tuple T ).

Lemma sub_tprod_lexi d n (T : preorderType disp) :
   subrel (<=%O : rel (n .-tupleprod [d ] T)) (<=%O : rel (n .-tuple T)).

End TupleLexiOrder.

Module Exports.

Notation "n .-tuplelexi[ disp ]" := (type disp n)
  (format "n .-tuplelexi[ disp ]") : type_scope.
Notation "n .-tuplelexi" := (type_ n)
  (format "n .-tuplelexi") : type_scope.

Definition topEtlexi := @topEtlexi.
Definition botEtlexi := @botEtlexi.
Definition sub_tprod_lexi := @sub_tprod_lexi.

End Exports.
End TupleLexiOrder.

Module DefaultTupleLexiOrder.
Section DefaultTupleLexiOrder.
Context {disp : disp_t}.

Notation "n .-tuplelexi" := n.-tuplelexi [seqlexi_display disp ].

End DefaultTupleLexiOrder.
End DefaultTupleLexiOrder.

We declare an alias of the sets, which is canonically ordered by inclusion

Module SetSubsetOrder.
Section SetSubsetOrder.

Fact subset_display : disp_t.

Definition type (disp : disp_t) (T : finType) := {set T }.

Context {disp : disp_t} {T : finType}.
Local Notation "{ 'subset' T }" := (type disp T).
Implicit Type (A B C : {subset T }).

Lemma le_def A B : A \subset B = (A :&: B == A ).

#[export ]
HB.instance Definition _ := Choice.on {subset T }.

#[export ]
HB.instance Definition _ := Le_isPreorder.Build disp {subset T }
  (@subxx _ _) (fun A B ⇒ @subset_trans _ B A ).

#[export ]
HB.instance Definition _ := hasBottom.Build disp {subset T } (@sub0set _).

#[export ]
HB.instance Definition _ := hasTop.Build disp {subset T } (@subsetT _).

Lemma leEsubset A B : (A ≤ B ) = (A \subset B ).

End SetSubsetOrder.

Module Exports.
Arguments type disp T%_type.
Notation "{ 'subset' [ d ] T }" := (type d T)
  (format "{ 'subset' [ d ] T }") : type_scope.
Notation "{ 'subset' T }" := {subset [subset_display ] T}
  (format "{ 'subset' T }") : type_scope.

Definition leEsubset := @leEsubset.

End Exports.
End SetSubsetOrder.
Export SetSubsetOrder.Exports.

Module DefaultSetSubsetOrder.

End DefaultSetSubsetOrder.

Notation enum A := (sort <=%O (enum A)).

Section Enum.
Variables (d : disp_t) (T : finPreorderType d).

Lemma cardE (A : {pred T }) : #|A | = size (enum A).

Lemma mem_enum (A : {pred T }) : enum A =i A.

Lemma enum_uniq (A : {pred T }) : uniq (enum A).

Lemma cardT : #|T | = size (enum T).

Lemma enumT : enum T = sort <=%O (Finite.enum T).

Lemma enum0 : enum (pred0 : {pred T }) = [::].

Lemma enum1 (x : T) : enum (pred1 x) = [:: x ].

Lemma eq_enum (A B : {pred T }) : A =i B → enum A = enum B.

Lemma eq_cardT (A : {pred T }) : A =i predT → #|A | = size (enum T).

Lemma set_enum (A : {set T }) : [set x in enum A ] = A.

Lemma enum_set0 : enum (set0 : {set T }) = [::].

Lemma enum_setT : enum [set : T ] = sort <=%O (Finite.enum T).

Lemma enum_set1 (a : T) : enum [set a ] = [:: a ].

End Enum.

Section Ordinal.
Import OrdinalOrder.Exports.

Lemma enum_ord n : enum 'I_n = fintype.enum 'I_n.

Lemma val_enum_ord n : [seq val i | i <- enum 'I_n ] = iota 0 n.

Lemma size_enum_ord n : size (enum 'I_n) = n.

Lemma nth_enum_ord (n : nat) (i0 : 'I_n) (m : nat) :
  (m < n)%N → nth i0 (enum 'I_n) m = m :> nat.

Lemma nth_ord_enum (n : nat) (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i.

Lemma index_enum_ord (n : nat) (i : 'I_n) : index i (enum 'I_n) = i.

End Ordinal.

Lemma mono_sorted_enum d d' (T : finPreorderType d)
    (T' : preorderType d') (f : T → T') :
    total (<=%O : rel T) → {mono f : x y / (x ≤ y)%O} →
  sorted <=%O [seq f x | x <- enum T ].

This module should be exported on demand, as in module tagnat below

Module Import EnumVal.
Section EnumVal.
Import OrdinalOrder.Exports.
Variables (d : disp_t) (T : finPreorderType d).
Implicit Types (x : T) (A : {pred T }).

Definition enum_rank_in x0 A (Ax0 : x0 \in A) x :=
  insubd (Ordinal (@enum_rank_subproof _ x0 A Ax0)) (index x (enum A)).

Definition enum_rank x := @enum_rank_in x T (erefl true) x.

Definition enum_val A i := nth (@enum_default _ A i) (enum A) i.

Lemma enum_valP A i : @enum_val A i \in A.

Lemma enum_val_nth A x i : @enum_val A i = nth x (enum A) i.

Lemma nth_enum_rank_in x00 x0 A Ax0 :
  {in A , cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))}.

Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).

Lemma enum_rankK_in x0 A Ax0 :
   {in A , cancel (@enum_rank_in x0 A Ax0) enum_val }.

Lemma enum_rankK : cancel enum_rank enum_val.

Lemma enum_valK_in x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0).

Lemma enum_valK : cancel enum_val enum_rank.

Lemma enum_rank_inj : injective enum_rank.

Lemma enum_val_inj A : injective (@enum_val A).

Lemma enum_val_bij_in x0 A : x0 \in A → {on A , bijective (@enum_val A )}.

Lemma eq_enum_rank_in (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
  {in A , enum_rank_in Ax0 =1 enum_rank_in Ay0 }.

Lemma enum_rank_in_inj (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
  {in A &, ∀ x y, enum_rank_in Ax0 x = enum_rank_in Ay0 y → x = y }.

Lemma enum_rank_bij : bijective enum_rank.

Lemma enum_val_bij : bijective (@enum_val T).

End EnumVal.
Arguments enum_val {d T A}.
Arguments enum_rank {d T}.
End EnumVal.

Notation enum_val := enum_val.
Notation enum_rank_in := enum_rank_in.
Notation enum_rank := enum_rank.
Notation enum_valP := enum_valP.
Notation enum_val_nth := enum_val_nth.
Notation nth_enum_rank_in := nth_enum_rank_in.
Notation nth_enum_rank := nth_enum_rank.
Notation enum_rankK_in := enum_rankK_in.
Notation enum_rankK := enum_rankK.
Notation enum_valK_in := enum_valK_in.
Notation enum_valK := enum_valK.
Notation enum_rank_inj := enum_rank_inj.
Notation enum_val_inj := enum_val_inj.
Notation enum_val_bij_in := enum_val_bij_in.
Notation eq_enum_rank_in := eq_enum_rank_in.
Notation enum_rank_in_inj := enum_rank_in_inj.
Notation enum_rank_bij := enum_rank_bij.
Notation enum_val_bij := enum_val_bij.

Module Syntax.
Export PreOSyntax.
Export DualSyntax.
Export DvdSyntax.
End Syntax.

Module Theory.
Export PreorderTheory.
Export PreOCoercions.
Export BPreorderTheory.
Export TPreorderTheory.
Export DualPreorder. (* FIXME? *)

Export OrderMorphismTheory.

Export SubPreorderTheory.
End Theory.

Module Exports.
End Exports.

End Order.

Export Order.Exports.

Export Order.Syntax.

Export Order.Preorder.Exports.
Export Order.BPreorder.Exports.
Export Order.TPreorder.Exports.
Export Order.TBPreorder.Exports.
Export Order.FinPreorder.Exports.
Export Order.FinBPreorder.Exports.
Export Order.FinTPreorder.Exports.
Export Order.FinTBPreorder.Exports.

FIXME: check if covered by Order.Exports Export Order.NatOrder.Exports. Export Order.NatMonotonyTheory. Export Order.NatDvd.Exports. Export Order.OrdinalOrder.Exports. Export Order.BoolOrder.Exports. Export Order.ProdOrder.Exports. Export Order.SigmaOrder.Exports. Export Order.ProdLexiOrder.Exports. Export Order.SeqProdOrder.Exports. Export Order.SeqLexiOrder.Exports. Export Order.TupleProdOrder.Exports. Export Order.TupleLexiOrder.Exports.

Module DefaultProdOrder := Order.DefaultProdOrder.
Module DefaultSeqProdOrder := Order.DefaultSeqProdOrder.
Module DefaultTupleProdOrder := Order.DefaultTupleProdOrder.
Module DefaultProdLexiOrder := Order.DefaultProdLexiOrder.
Module DefaultSeqLexiOrder := Order.DefaultSeqLexiOrder.
Module DefaultTupleLexiOrder := Order.DefaultTupleLexiOrder.