# Theory of Sets EIII-1 Order relations. Ordered sets

Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm).

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset4.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Border.

## EIII-1-1 Definition of an order relation

Definitions are given in sset4

Lemma equality_order_r: order_r (fun x y => x = y).
Proof.
split; first (by move => y x z -> ->); move => x y //=.
Qed.

Lemma sub_order_r: order_r sub.
Proof.
split; first by move=> x y t xy yz; apply: (sub_trans xy yz).
by move=> x y xy yx; apply: extensionality.
move=> x y; split; apply: sub_refl.
Qed.

The opposite of r x y is the relation r y x. A symmetric relation is equal to its opposite. The opposite of an order relation is an order relation

Definition opposite_relation (r:relation) := fun x y => r y x.

Lemma opposite_preorder_r r: preorder_r r -> preorder_r (opposite_relation r).
Proof.
rewrite /preorder_r/opposite_relation; move => [tr rr].
split; first by move=> x y z xy yz; apply: tr yz xy.
by move=> x y /rr [].
Qed.

Lemma opposite_order_r r: order_r r -> order_r (opposite_relation r).
Proof.
move=> [tr ar rr].
have: preorder_r r by [].
move /opposite_preorder_r => [tr' rr'].
by split => // x y xy yx; apply: (ar _ _ yx).
Qed.

An order is the graph of an order relation

Lemma order_from_rel1 r x:
transitive_r r ->
(forall u v, inc u x -> inc v x -> r u v -> r v u -> u = v) ->
(forall u, inc u x -> r u u) ->
order (graph_on r x).
Proof.
move=> tr sy re.
have ->: (graph_on r x = graph_on (fun a b => [/\ inc a x, inc b x & r a b]) x).
by apply: Zo_exten1 => t /setX_P [_ px qx]; split => // [] [_ _].
apply: order_from_rel; split.
move => a b c [ax bx rab] [_ cx rbc]; split => //; apply: tr rab rbc.
by move=> a b [ax bx rab] [_ cx rbc]; apply: sy.
by move=> a b [ax bx rab];split => //; split => //; apply: re.
Qed.

We define gle r x y and glt r x y

Definition gle r x y := related r x y.
Definition glt r x y := gle r x y /\ x <> y.

Lemma order_reflexivityP r: order r ->
forall a, (inc a (substrate r) <-> gle r a a).
Proof.
move=> [_ or _ _]; rewrite /gle;split => h; [by apply: or | substr_tac].
Qed.

Lemma order_antisymmetry r a b:
order r -> gle r a b -> gle r b a -> a = b.
Proof. move=> [_ _ _]; apply. Qed.

Lemma order_transitivity r a b c:
order r -> gle r a b -> gle r b c -> gle r a c.
Proof. move=> [_ _ t _]; apply: t. Qed.

Lemma lt_leq_trans r x y z:
order r -> glt r x y -> gle r y z -> glt r x z.
Proof.
move=> or [le1 nxy] le2; split; first by apply: order_transitivity le1 le2.
dneg xz; rewrite -xz in le2.
apply: (order_antisymmetry or le1 le2).
Qed.

Lemma leq_lt_trans r x y z:
order r -> gle r x y -> glt r y z -> glt r x z.
Proof.
move=> or le1 [le2 nxy]; split; first by apply: order_transitivity le1 le2.
dneg xz; rewrite xz in le1.
apply: (order_antisymmetry or le2 le1).
Qed.

Lemma lt_lt_trans r a b c:
order r -> glt r a b -> glt r b c -> glt r a c.
Proof. move=> or [le1 _] le2; apply: (leq_lt_trans or le1 le2). Qed.

Lemma not_le_gt r x y: order r -> gle r x y -> glt r y x -> False.
Proof.
by move=> or le1 le2; move: (leq_lt_trans or le1 le2) => [_]; case.
Qed.

Lemma order_exten r r': order r -> order r' ->
(forall x y, gle r x y <-> gle r' x y) -> (r = r').
Proof. by move=> or or'; apply: sgraph_exten; fprops. Qed.

A tactic that uses properties of order

Ltac order_tac:=
match goal with
| H1: gle ?r ?x _ |- inc ?x (substrate ?r)
=> exact (arg1_sr H1)
| H1: glt ?r ?x _ |- inc ?x (substrate ?r)
=> move: H1 => [H1 _] ; order_tac
| H1:gle ?r _ ?x |- inc ?x (substrate ?r)
=> exact (arg2_sr H1)
| H1:glt ?r _ ?x |- inc ?x (substrate ?r)
=> move: H1 => [H1 _]; order_tac
| H: order ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u
=> rewrite -/gle; apply /(order_reflexivityP H)
| H: order ?r |- inc (J ?u ?u) ?r
=> change (gle r u u); apply /(order_reflexivityP H)
| H: order ?r |- gle ?r ?u ?u
=> apply /(order_reflexivityP H)
| H1: gle ?r ?x ?y, H2: gle ?r ?y ?x, H:order ?r |-
?x = ?y => exact (order_antisymmetry H H1 H2)
| H:order ?r, H1:related ?r ?x ?y, H2: related ?r ?y ?x |- ?x = ?y
=> apply (order_antisymmetry H H1 H2)
| H:order ?r, H1: inc (J ?x ?y) ?r , H2: inc (J ?y ?x) ?r |- ?x = ?y
=> apply (order_antisymmetry H H1 H2)
| H:order ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w
|- related ?r ?u ?w
=> apply (order_transitivity H H1 H2)
| H:order ?r, H1:gle ?r ?u ?v, H2: gle ?r ?v ?w |- gle ?r ?u ?w
=> apply (order_transitivity H H1 H2)
| H: order ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |-
inc (J ?u ?w) ?r
=> change (related r u w); apply (order_transitivity H H1 H2)
| H1: gle ?r ?x ?y, H2: glt ?r ?y ?x, H: order ?r |- _
=> case: (not_le_gt H H1 H2)
| H1:glt ?r ?x ?y, H2: glt ?r ?y ?x, H:order ?r |- _
=> move: H1 => [H1 _] ; case: (not_le_gt H H1 H2)
| H1:order ?r, H2:glt ?r ?x ?y, H3: gle ?r ?y ?z |- glt ?r ?x ?z
=> exact (lt_leq_trans H1 H2 H3)
| H1:order ?r, H2:gle ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
=> exact (leq_lt_trans H1 H2 H3)
| H1:order ?r, H2:glt ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
=> exact (lt_lt_trans H1 H2 H3)
| H1:order ?r, H2:gle ?r ?x ?y |- glt ?r ?x ?y
=> split =>//
| H:glt ?r ?x ?y |- gle ?r ?x ?y
=> by move: H=> []
end.

The opposite of an order is the inverse graph

Definition opp_order := inverse_graph.

Lemma opp_gleP r x y: gle (opp_order r) x y <-> gle r y x.
Proof. exact: igraph_pP. Qed.

Lemma opp_gltP r x y: glt (opp_order r) x y <-> glt r y x.
Proof. by split; move => [] /opp_gleP pa pb; split => //; dneg h. Qed.

Lemma opp_osr r: order r -> order_on (opp_order r) (substrate r).
Proof.
move => osr.
have go: sgraph (opp_order r) by fprops.
have pc: substrate (opp_order r) = (substrate r).
set_extens x.
case/(substrate_P go) => [][y]; move/igraph_pP =>h; substr_tac.
by move => xsr; apply /substr_i /igraph_pP /(order_reflexivityP osr).
split => //;split; first by fprops.
move => t; rewrite pc => yg.
by apply/opp_gleP; order_tac.
move => x y z /opp_gleP pa /opp_gleP pb; apply/opp_gleP; order_tac.
move => x y /opp_gleP pa /opp_gleP pb; order_tac.
Qed.

Inclusion order on the powerset of a set, or a part of it

Definition sub_order := graph_on sub.
Definition subp_order E := sub_order (powerset E).

Lemma sub_osr A: order_on (sub_order A) A.
Proof.
split; first by apply: order_from_rel; apply: sub_order_r.
by apply: graph_on_sr; move=> x; fprops.
Qed.

Lemma subp_osr E: order_on (subp_order E) (powerset E).
Proof. exact: sub_osr. Qed.

Lemma sub_gleP A u v:
gle (sub_order A) u v <-> [/\ inc u A, inc v A & sub u v].
Proof. by apply /graph_on_P1. Qed.

Lemma subp_gleP E u v:
gle (subp_order E) u v <-> [/\ sub u E, sub v E & sub u v].
Proof.
split; first by move /graph_on_P1 => [] /setP_P pa /setP_P pb.
by move => [pa pb pc]; apply /graph_on_P1;split => //; apply/setP_P.
Qed.

Extension order on partial functions from x to y

Definition extension_order E F :=
graph_on extends (sub_functions E F).

Lemma extension_osr E F:
order_on (extension_order E F) (sub_functions E F).
Proof.
split; last by apply: graph_on_sr => a /sfun_set_P [pa pb pc]; split; fprops.
apply: order_from_rel.
split.
- move=> a b c [fa fb gba tba] [fc _ gcb tcb].
split => //; first by apply: sub_trans gba.
by apply: sub_trans tba.
- move=> a b [fb fa gba tba] [_ _ gab tab].
have grab: graph a = graph b by apply: extensionality.
have tgab: target a = target b by apply: extensionality.
by apply: function_exten1.
- move => a b [fa fb _ _ ]; split; split;fprops.
Qed.

Lemma extension_orderP E F f g:
gle (extension_order E F) g f <->
[/\ inc g (sub_functions E F), inc f (sub_functions E F)
& extends g f].
Proof. apply /graph_on_P0. Qed.

Lemma extension_order_P1 E F f g:
gle (extension_order E F) g f <->
[/\ inc g (sub_functions E F), inc f (sub_functions E F)
& sub (graph f) (graph g)].
Proof.
split; first by move/extension_orderP => [pa pb [_ _ pd _]].
move=> [p1 p2 sh]; apply/extension_orderP; split=>//.
move: p1 p2 => /sfun_set_P [fg _ tg] /sfun_set_P [ff _ tf].
split => //; rewrite tg tf;fprops.
Qed.

Lemma extension_order_P2 E F f g:
gle (opp_order (extension_order E F)) g f <->
[/\ inc g (sub_functions E F), inc f (sub_functions E F)
& sub (graph g) (graph f)].
Proof.
split; first by move/opp_gleP /extension_order_P1=> [pa pb pc].
by move => [pa pb pc]; apply/opp_gleP /extension_order_P1.
Qed.

Lemma extension_order_pr E F f g x:
gle (opp_order (extension_order E F)) f g ->
inc x (source f) -> Vf f x = Vf g x.
Proof.
move/opp_gleP/extension_orderP=> [gs fs et] xsf; exact: (extends_sV et xsf).
Qed.

Example 4. Order between partitions on a set

Definition partitions E :=
Zo (powerset(powerset E)) (fun z => partition_s z E).

Definition part_fun p E := canonical_injection p (powerset E).

Lemma partition_set_in_PP p E:
partition_s p E -> inc p (powerset (powerset E)).
Proof.
by move=> [[<- _] _ ]; apply /setP_P => t ty;apply/setP_P; apply: setU_s1.
Qed.

Lemma partitionsP p E:
inc p (partitions E) <-> partition_s p E.
Proof.
by split; [move/Zo_hi|move => h;apply/Zo_i=> //; apply: partition_set_in_PP].
Qed.

Lemma pfs_f p E: partition_s p E -> function (part_fun p E).
Proof.
by move=> pa; apply: ci_f; apply/setP_P;apply: partition_set_in_PP.
Qed.

Lemma pfs_V p E a: partition_s p E -> inc a p -> Vf (part_fun p E) a = a.
Proof.
by move => pa; apply: ci_V => //; apply/setP_P; apply: partition_set_in_PP.
Qed.

Lemma pfs_partition p E:
partition_s p E -> partition_w_fam (graph (part_fun p E)) E.
Proof.
move=> pa.
move: (pfs_f pa) => fpa.
move: (pa)=> [[ux di] _].
have Wp: forall i, inc i p -> Vg (graph (part_fun p E)) i = i.
by move => i iy; apply: pfs_V.
have dg: domain (graph (part_fun p E)) = p.
by rewrite f_domain_graph// /part_fun /canonical_injection; aw.
split; fprops.
by move=> i j; rewrite dg => iy jy; rewrite Wp // Wp //; apply: di.
set_extens v => vs.
move: (setUb_hi vs)=> [w]; rewrite dg.
move=> wy; rewrite Wp // -ux => vW; union_tac.
rewrite -ux in vs; move: (setU_hi vs) => [w vw wy].
by apply /setUb_P; exists w; rewrite ? dg ? (Wp _ wy).
Qed.

The relation coarser_cs is an ordering on the set of partitions. We know the greatest and least element

Definition coarser x := graph_on coarser_cs (partitions x).

Lemma coarser_gleP x y y':
gle (coarser x) y y' <->
[/\ partition_s y x, partition_s y' x & coarser_cs y y'].
Proof.
split.
by move/Zo_P => [/setXp_P [/partitionsP pa /partitionsP pb]]; aw.
move => [pa pb pc]; apply: Zo_i; aw.
by apply /setXp_P; split;apply /partitionsP.
Qed.

Lemma coarser_osr x: order_on (coarser x) (partitions x).
Proof.
have sr :substrate (coarser x) = partitions x.
apply: extensionality; first by apply: graph_on_sr1.
move => t ts.
apply: (@arg1_sr _ t t); apply:Zo_i.
by apply/setXp_P; split.
aw; apply: coarserR.
split=> //;split.
- by rewrite /coarser; apply: graph_on_graph.
- red; rewrite sr => y h; move /partitionsP: (h) => h'.
apply/coarser_gleP;split => //; apply: coarserR.
- move=> a b c /coarser_gleP [pa _ ab] /coarser_gleP [_ pb bc].
apply /coarser_gleP;split => //; apply: (coarserT ab bc).
- move=> a b /coarser_gleP [pa _ ab] /coarser_gleP [pb _ ba].
apply: (coarserA pa pb ab ba).
Qed.

Lemma least_partition_is_least x y:
nonempty x ->
partition_s y x -> gle (coarser x) (least_partition x) y.
Proof.
move=> nex pa;apply/coarser_gleP;split => //; first by apply:least_is_partition.
move=> u uy; rewrite /least_partition.
by ex_tac; move:(partition_set_in_PP pa) => /setP_P yp; apply/setP_P; apply: yp.
Qed.

Lemma greatest_partition_is_greatest x y:
partition_s y x -> gle (coarser x) y (greatest_partition x).
Proof.
move=> pa; move: (pa) => [[pb _] _]; apply /coarser_gleP.
split => //; first by apply: greatest_is_partition.
move=> u /funI_P [b bx ->].
by move: bx; rewrite -pb;move /setU_P=> [z bz zy];ex_tac; move=> t /set1_P ->.
Qed.

Assume that y is a partition of x; we deduce an equivalence on x. The union of all coarse a for a in y is the graph of this equivalence

Definition partition_relset y x :=
partition_relation (part_fun y x) x.

Lemma prs_is_equivalence y x:
partition_s y x -> equivalence (partition_relset y x).
Proof.
move=> pa; apply: isc_rel_equivalence; first by apply: pfs_f.
by apply: pfs_partition.
Qed.

Definition partition_relset_aux y x :=
Zo (powerset (coarse x)) (fun z => exists2 a, inc a y & z = coarse a).

Lemma partition_relset_pr1 y x a:
partition_s y x ->
inc a y -> inc (coarse a) (partition_relset_aux y x).
Proof.
move=> pa ay.
move /setP_P: (partition_set_in_PP pa) => yp.
apply:Zo_i; last by ex_tac.
by apply /setP_P; apply:setX_Sll; apply/setP_P; apply: yp.
Qed.

Lemma partition_relset_pr y x:
partition_s y x ->
partition_relset y x = union (partition_relset_aux y x).
Proof.
move=> pa.
have pfa: (partition_w_fam (graph(part_fun y x)) x) by apply: pfs_partition.
have sp:source (part_fun y x) = y by rewrite /part_fun /canonical_injection;aw.
move: (partition_set_in_PP pa); aw => ypp.
have p1: function (part_fun y x) by apply: pfs_f.
have p2: partition_w_fam (graph (part_fun y x)) x.
by move: (prs_is_equivalence pa); fprops.
have p3: sgraph (partition_relation (part_fun y x) x).
by rewrite /partition_relation; apply: graph_on_graph.
have p4:sgraph (union (partition_relset_aux y x)).
move=> t tp; move: (setU_hi tp); rewrite/partition_relset_aux.
by move=> [z tz /Zo_P [] /setP_P zp _]; move: (zp _ tz) => /setX_P [].
apply: sgraph_exten => //.
move=> u v; split.
move /(isc_rel_P p1 p2); rewrite /in_same_coset // sp.
move=> [i [iy ]]; rewrite pfs_V // => ui vi.
apply (@setU_i _ (coarse i)); first by rewrite/coarse; fprops.
by apply: partition_relset_pr1.
move/setU_P => [z pz] /Zo_P [zp [a ay zc]].
move: pz; rewrite zc; move /setXp_P => [ua va].
by apply/(isc_rel_P p1 p2); red;rewrite sp; exists a;split => //; rewrite pfs_V.
Qed.

Lemma sub_part_relsetX y x:
partition_s y x -> sub (partition_relset y x) (coarse x).
Proof.
move=> pa; rewrite partition_relset_pr // => t tu.
by move: (setU_hi tu) => [z tz /Zo_P [/setP_P zp _ ]]; apply: zp.
Qed.

A partition y is coarser than y if sub z' z where z and z' are the associated equivalence

Lemma partition_relset_order x y y':
partition_s y x -> partition_s y' x ->
(sub (partition_relset y' x)(partition_relset y x) <->
gle (coarser x) y y').
Proof.
move=> pa pa'.
do 2 rewrite partition_relset_pr //.
split; last first.
move /coarser_gleP=> [_ _ hyp] z /setU_hi [t zt /Zo_P [tp [a ay tc]]].
move: (hyp _ ay)=> [b iby ab].
apply: (@setU_i _ (coarse b)); last by apply: partition_relset_pr1.
by apply (setX_Sll ab); ue.
move => suu; apply/coarser_gleP;split=>//; move=> a ay.
have [b ba]: (nonempty a) by apply (proj2 pa').
have p: (forall u, inc u a -> exists c, [/\ inc c y, inc b c& inc u c]).
move=> u ua.
have q: (inc (J b u) (union (partition_relset_aux y' x))).
apply: (@setU_i _ (coarse a)); first by rewrite /coarse; fprops.
apply: (partition_relset_pr1 pa' ay).
move : (setU_hi (suu _ q)) => [z Jbb /Zo_P [zp [c cy zc]]].
by move: Jbb; rewrite zc; move/setXp_P=> [s1 s2]; exists c.
move: (p _ ba) => [c [cy bc _]]; ex_tac.
move=> d /p [f [fy bf df]].
case: (proj2 (proj1 pa) _ _ cy fy); first by move => ->.
by move=> dcf; case: (nondisjoint bc bf dcf).
Qed.

Lemma part_relset_anti x y y':
partition_s y x -> partition_s y' x ->
(partition_relset y' x = partition_relset y x) ->
y = y'.
Proof.
move: x y y'.
suff: (forall x y y',
partition_s y x -> partition_s y' x ->
(partition_relset y' x = partition_relset y x) ->
sub y y').
move=> aux a b c p1 p2 eq; apply: extensionality.
apply: aux p1 p2 eq.
apply: aux p2 p1 (sym_eq eq).
move=> x y y' pa pa'.
rewrite (partition_relset_pr pa) (partition_relset_pr pa').
move=> eq a ay.
move: (partition_relset_pr1 pa ay)=> cpy.
have [b ba] := (proj2 pa _ ay).
have p: (forall u v,inc u a -> inc v a ->
exists c, [/\ inc c y', inc u c & inc v c]).
move=> u v ua va.
have p1: inc (J u v) (coarse a) by rewrite /coarse; fprops.
have p2: (inc (J u v) (union (partition_relset_aux y' x))).
rewrite eq; union_tac.
move: (setU_hi p2) => [z Jbb /Zo_P [zp [c cy zc]]].
by exists c; split=> //; move: Jbb; rewrite zc; move/setXp_P => [].
move: (p _ _ ba ba) => [c [cy bc _]].
suff: a = c by move=> ->.
set_extens t => ta.
move: (p _ _ ta ta) => [c' [cy' tc' _]].
move: (p _ _ ba ta) => [c'' [cy'' bc'' tc'']].
case:((proj2 (proj1 pa') )_ _ cy cy'').
move => ->; case:((proj2 (proj1 pa')) _ _ cy'' cy'); first by move => ->.
by move=> dcf;case: (nondisjoint tc'' tc' dcf).
by move=> dcf;case: (nondisjoint bc bc'' dcf).
have p1: (inc (J b t) (coarse c)) by rewrite/coarse; fprops.
have p2: (inc (J b t) (union (partition_relset_aux y' x))).
apply: (setU_i p1); apply: (partition_relset_pr1 pa' cy).
move: p2; rewrite eq /partition_relset_aux => p2.
move: (setU_hi p2)=> [z Jbb /Zo_P [zp [d dy zx]]].
move: Jbb; rewrite zx; move/setXp_P => [bd td].
case:((proj2 (proj1 pa)) _ _ ay dy); first by move=> ->.
move=> dfc; case: (nondisjoint ba bd dfc).
Qed.

Characterisation of graphs of orders and preorders.

Lemma preorder_prop1 g:
sgraph g ->
sub (diagonal (substrate g)) g -> sub (g \cg g) g ->
g \cg g = g.
Proof.
move=> gg sig scg; apply: extensionality; first by aw.
move => x xg; apply /compg_P; split; first by apply: gg.
exists (Q x); rewrite ? (gg _ xg) //;apply: sig; apply/diagonal_pi_P.
split => //;substr_tac.
Qed.

Lemma preorderP g:
sgraph g ->
(preorder g <-> (sub (diagonal (substrate g)) g /\ sub (g \cg g) g)).
Proof.
move=> gg.
split.
move=> [_ rr tr]; split; move=> x.
by move/diagonal_i_P=> [px Px pq]; rewrite -px -pq; apply: rr.
move: tr;rewrite idempotent_graph_transitive //; apply.
move=> [s1 s2];split=> //.
by move=> y ys; apply: s1; apply/diagonal_pi_P.
by rewrite idempotent_graph_transitive.
Qed.

Theorem orderP r:
order r <->
(r \cg r = r /\
r \cap (opp_order r) = diagonal (substrate r)).
Proof.
split.
move=> or.
set (d:= diagonal (substrate r)).
have i2: (r \cap (opp_order r) = d).
set_extens t.
move /setI2_P => [tr /igraphP [pt Jr]].
apply /diagonal_i_P;split => //; first by substr_tac.
rewrite -pt in tr; apply: (order_antisymmetry or tr Jr).
move/diagonal_i_P => [pt Ps pq].
rewrite -pt -pq.
have rpp: (related r (P t) (P t)) by order_tac.
by apply: setI2_i=>//; apply/igraph_pP.
have gr: (sgraph r) by fprops.
have sd: (sub d r) by rewrite -i2; apply : setI2_1.
have sc: (sub (d \cg r) (r \cg r)) by apply: compg_S; fprops.
have crrr: (sub (r \cg r) r).
move: or => [_ _ t _];rewrite -idempotent_graph_transitive //.
by split =>//; apply: preorder_prop1.
move=> [crrr iro].
have sr: sgraph r by rewrite -crrr; apply: compg_graph.
split=> //.
- move=> y ys.
have: (inc (J y y) (diagonal (substrate r))) by apply /diagonal_pi_P.
by rewrite -iro; move=> Ji; apply: (setI2_1 Ji).
- have: sub (r \cg r) r by rewrite crrr; fprops.
rewrite -idempotent_graph_transitive //.
- move => x y rxy ryx.
have p1: (inc (J x y) (opp_order r)) by apply/igraph_pP.
have: (inc (J x y) (diagonal (substrate r))).
by rewrite - iro; apply: setI2_i.
by move /diagonal_pi_P => [_].
Qed.

Lemma order_structure s a:
inc s (powerset(coarse a)) ->
s \cg s = s ->
s \cap (inverse_graph s) = diagonal a ->
a = substrate s.
Proof.
move => /setP_P pa pb pc; set_extens t => ta.
have : inc (J t t) (diagonal a) by apply /diagonal_pi_P.
rewrite -pc => /setI2_P [ts _]; substr_tac.
have sg: sgraph s by rewrite - pb; fprops.
by case /(substrate_P sg): ta => [] [y ps]; move: (pa _ ps) => /setXp_P [pd pe].
Qed.

## Preorder relations

Lemma preorder_reflexivity r a:
preorder r -> (inc a (substrate r) <-> gle r a a).
Proof.
move=> [g pr _]; split; first by apply: pr.
rewrite/gle;move=> h; substr_tac.
Qed.

Lemma opposite_is_preorder1 r:
preorder r -> preorder (opp_order r).
Proof.
move=> [gr rr tr].
have go: (sgraph (opp_order r)) by fprops.
have ss: (sub (substrate (opp_order r)) (substrate r)).
move=> t /(substrate_P go) [] [y] /igraph_pP => h; substr_tac.
split => //.
by move=> y ys; apply /igraph_pP;apply: rr; apply: ss.
move => x y z /igraph_pP p1 /igraph_pP p2; apply /igraph_pP.
apply: tr p2 p1.
Qed.

r x y /\ r y x is an equivalence relation, compatible with r

Definition symmetrize (r: relation) := fun x y => r x y /\ r y x.

Lemma equivalence_preorder r:
preorder_r r -> equivalence_r (symmetrize r).
Proof.
move=> [ tr _]; split; first by move=> x y [rxy ryx].
move=> x y z [xy yx] [yz zy].
split; [ apply: tr xy yz | apply: tr zy yx].
Qed.

Lemma compatible_equivalence_preorder r (s := symmetrize r):
preorder_r r -> forall x y x' y', r x y -> s x x' -> s y y' -> r x' y'.
Proof.
move=> [tr _] x y x' y' rxy [rxx' rx'x] [ryy' ry'y].
move: (tr _ _ _ rx'x rxy) => rx'y.
apply: tr rx'y ryy'.
Qed.

This is the graph of the equivalence associated

Definition equivalence_associated_o r:= r \cap (opp_order r).

Lemma eao_P r x y:
related (equivalence_associated_o r) x y <-> symmetrize (gle r) x y.
Proof.
split; first by move /setI2_P =>[pa] /igraph_pP pb; split.
by move => [pa pb]; apply:setI2_i => //; apply /igraph_pP.
Qed.

Lemma equivalence_preorder1 r:
preorder r ->
equivalence (equivalence_associated_o r).
Proof.
move=> [gr _ tr].
have gi: sgraph (opp_order r) by fprops.
move: (setI2_graph2 gr (x:=r)) => gi2.
have gi3: sgraph (r \cap (opp_order r)).
by move=> x xi; apply: gr (setI2_1 xi).
apply: symmetric_transitive_equivalence => //.
by move=> x y /eao_P [pa pb]; apply/eao_P.
move=> x y z /eao_P [xy yx] /eao_P [yz zy]; apply/eao_P.
split; [ apply: tr xy yz | apply: tr zy yx ].
Qed.

Lemma equivalence_associated_o_sr r:
preorder r ->
substrate (equivalence_associated_o r) = substrate r.
Proof.
move=> pr.
move: (equivalence_preorder1 pr)=> eq.
set_extens x => xs.
move: (reflexivity_e eq xs) => /eao_P [pa _]; order_tac.
move: pr=> [gr rr _].
by apply: substr_i;move : (rr _ xs) => t;apply/eao_P; split.
Qed.

Lemma compatible_equivalence_preorder1 r u v x y:
preorder r -> related r x y ->
related (equivalence_associated_o r) x u ->
related (equivalence_associated_o r) y v ->
related r u v.
Proof.
move => pr rxy /eao_P [_ pb] /eao_P [pc _].
move: pr => [_ _ tr]; apply: tr (tr _ _ _ pb rxy) pc.
Qed.

If r is a preorder, e the associated equivalence, E the quotient, the relation induced by r on E is an ordering

Definition order_associated r :=
let s := graph (canon_proj (equivalence_associated_o r)) in
(s \cg r) \cg (opp_order s).

Lemma oap_graph r: sgraph (order_associated r).
Proof. apply: compg_graph. Qed.

Lemma compose3_relP s r u v:
related ((s \cg r) \cg (opp_order s)) u v <->
exists x, exists y, [/\ related s x u, related s y v& related r x y].
Proof.
split.
by move/compg_pP => [z /igraph_pP pa /compg_pP [y pb pc]]; exists z, y.
move=> [x [y [xu yv xy]]]; apply/compg_pP;exists x.
by apply/igraph_pP.
by apply/compg_pP; exists y.
Qed.

Section OrderAssociated.
Variable (r:Set).
Hypothesis pr: preorder r.

Lemma oap_relP1 u v:
related (order_associated r) u v <->
[/\ inc u (quotient (equivalence_associated_o r)) ,
inc v (quotient (equivalence_associated_o r)) &
exists x, exists y, [/\ inc x u, inc y v & related r x y]].
Proof.
set s:= equivalence_associated_o r.
set p:= graph (canon_proj s).
rewrite /order_associated -/s -/p.
have es:equivalence s by apply: equivalence_preorder1.
split.
move /compose3_relP=> [x [y [xu yv xy]]].
have fc: function (canon_proj s) by apply: canon_proj_f.
move: (p1graph_source fc xu); aw => xs.
move: (p1graph_source fc yv); aw => ys.
have: (u = Vf (canon_proj s) x) by apply: Vf_pr.
have: (v = Vf (canon_proj s) y) by apply: Vf_pr.
rewrite canon_proj_V // canon_proj_V //.
move=> -> ->; split; fprops.
exists x; exists y; split => //; first by apply: inc_itself_class.
by apply: inc_itself_class.
move=> [uq vq [x [y [xu yv xy]]]]; apply /compose3_relP.
exists x; exists y; split => //.
apply/(rel_gcp_P es) => //; apply: (inc_in_setQ_sr es xu uq).
apply/(rel_gcp_P es) => //; apply: (inc_in_setQ_sr es yv vq).
Qed.

Lemma oap_relP2 u v:
related (order_associated r) u v <->
[/\ inc u (quotient (equivalence_associated_o r)),
inc v (quotient (equivalence_associated_o r)) &
forall x y, inc x u -> inc y v -> related r x y].
Proof.
set (s:= equivalence_associated_o r).
have es: equivalence s by rewrite /s; apply: equivalence_preorder1.
split.
move /oap_relP1 => [uq vq [x [y [xu yv xy]]]]; split=> //.
move=> a b au bv.
have xa: (related s x a).
by apply /(in_class_relatedP es); exists u; split => //;apply/(setQ_P es).
have yb: (related s y b).
by apply /(in_class_relatedP es); exists v;split => //; apply/(setQ_P es).
apply: (compatible_equivalence_preorder1 pr xy xa yb).
move => [uq vq hyp]; apply/oap_relP1;split => //.
move: (setQ_repi es uq) (setQ_repi es vq) => pa pb.
by exists (rep u); exists (rep v);split => //; apply: hyp.
Qed.

Lemma oap_osr:
order_on (order_associated r)(quotient (equivalence_associated_o r)).
Proof.
have ea:equivalence (equivalence_associated_o r).
by apply: equivalence_preorder1.
set eao:= (equivalence_associated_o r).
have prop: forall a b, inc (J a b) (order_associated r)->
(inc a (quotient eao) /\ inc b (quotient eao)).
move=> a b Jab.
have: (related (order_associated r) a b) by done.
by move/oap_relP2=> [pa pb _].
have sr:substrate (order_associated r) = quotient eao.
set_extens x.
move:(@oap_graph r) => h.
by move/(substrate_P h) => [][y /oap_relP2 [pa pb _]].
move=> xq; apply: substr_i;apply/oap_relP2; split => // z y zx yx.
suff: symmetrize (gle r) z y by move => [].
apply/eao_P; apply/(in_class_relatedP ea).
by exists x;split => //; apply/(setQ_P ea).
have go: sgraph (order_associated r) by apply: oap_graph.
split => //.
move:(pr)=> [rr gr tr]; split => //.
red; rewrite sr => y ys;apply/oap_relP2; split => // x z xy zy.
have: (related (equivalence_associated_o r) x z).
by apply/(in_class_relatedP ea); exists y; split=>//; apply/(setQ_P ea).
by move/eao_P=> [].
move=> x y z /oap_relP2 [xq yq rxy]/oap_relP2 [_ zq ryz].
apply/oap_relP2;split => // a b ax bz; move: (setQ_repi ea yq) => cy.
apply: tr (rxy _ _ ax cy) (ryz _ _ cy bz).
move=> x y /oap_relP2 [xq yq rxy] /oap_relP2 [_ _ ryx].
move:(setQ_repi ea xq) (setQ_repi ea yq) => ax biy.
move: (rxy _ _ ax biy)(ryx _ _ biy ax)=> rab rba.
move: (conj rab rba); move /eao_P=> reab.
move: xq yq => /(setQ_P ea) cx /(setQ_P ea) cy.
have bx: inc (rep y) x by apply: (rel_in_class2 ea cx reab).
case: (class_dichot ea cx cy) =>// hyp.
case: (nondisjoint bx biy hyp).
Qed.

Lemma oap_pr:
order_associated r = image_by_fun (
ext_to_prod(canon_proj (equivalence_associated_o r))
(canon_proj (equivalence_associated_o r))) r.
Proof.
set (s:= equivalence_associated_o r).
have es:equivalence s by rewrite /s; apply: equivalence_preorder1.
have ss:substrate s = substrate r.
by rewrite /s equivalence_associated_o_sr.
have fep: function (ext_to_prod (canon_proj s) (canon_proj s)).
by apply: ext_to_prod_f; apply: canon_proj_f.
have gi: sgraph (image_by_fun (ext_to_prod (canon_proj s) (canon_proj s)) r).
move=> t /dirim_P [x xr Jg].
by move:(p2graph_target fep Jg); rewrite lf_target; move/setX_P => [].
apply/sgraph_exten=> //; first by apply: oap_graph.
move=> u v; split.
move/oap_relP2=> [uq vq hyp]; apply/dirim_P;exists (J (rep u) (rep v)).
by apply: hyp; apply: (setQ_repi es).
have : (J u v = J (class s (rep u)) (class s (rep v))) by rewrite ! class_rep.
rewrite - ext_to_prod_rel_V; fprops; move =>->.
by apply: Vf_pr3=> //; rewrite /ext_to_prod; aw; fprops.
move/dirim_P=> [x xr Jg]; move: (Vf_pr fep Jg)=> Wx.
have px: (pairp x) by move: pr=> [g _ _]; apply: g.
have ps: (inc (P x) (substrate s)) by rewrite ss; substr_tac.
have qs: (inc (Q x) (substrate s)) by rewrite ss; substr_tac.
move: Wx; rewrite -px ext_to_prod_rel_V // => JJ.
rewrite (pr1_def JJ) (pr2_def JJ).
apply/oap_relP2;split;fprops => a b au bv.
suff: (related (order_associated r) (class s (P x)) (class s (Q x))).
by move /oap_relP2 => [_ _ h]; apply: h au bv.
apply /oap_relP1;split; fprops.
exists (P x), (Q x); split ; try apply: (inc_itself_class es) => //.
by red; rewrite px.
Qed.

End OrderAssociated.

## Notation and terminology

Bourbaki defines an ordering r of s to be a set satisfying the following condition

Definition order_axioms r s :=
[/\ (forall y x z, gle r x y -> gle r y z -> gle r x z),
(forall x y, gle r x y -> gle r y x -> x = y),
(forall x y, gle r x y -> (inc x s /\ inc y s)),
(forall x, gle r x x <-> inc x s) &
sgraph r].

Lemma axioms_of_order r:
order r <-> (order_axioms r (substrate r)).
Proof.
rewrite/order_axioms; split.
move => [p1 p2 p3 p4].
split => //.
by move => x y xy; split; order_tac.
by move => x; split => h; try order_tac; apply: p2.
move=> [h1 h2 h3 h4 gr]; split => //; by move => y /h4.
Qed.

A morphism is a function that preserves ordering. It is injective. When bijective it is called an isomorphism. We show stability by composition

Definition fincr_prop f r r' :=
forall x y, gle r x y -> gle r' (Vf f x) (Vf f y).
Definition fsincr_prop f r r' :=
forall x y, glt r x y -> glt r' (Vf f x) (Vf f y).

Definition fiso_prop f r r' :=
forall x y, inc x (source f) -> inc y (source f) ->
(gle r x y <-> gle r' (Vf f x) (Vf f y)).
Definition fsiso_prop f r r' :=
forall x y, inc x (source f) -> inc y (source f) ->
(glt r x y <-> glt r' (Vf f x) (Vf f y)).

Definition order_isomorphism f r r' :=
[/\ (order r), (order r'), bijection_prop f (substrate r) (substrate r')&
fiso_prop f r r'].

Definition order_morphism f r r' :=
[/\ (order r), (order r'), function_prop f (substrate r) (substrate r') &
fiso_prop f r r'].

Definition order_isomorphic r r':=
exists f, order_isomorphism f r r'.
Notation "x \Is y" := (order_isomorphic x y) (at level 50).

Lemma order_morphism_fi f r r': order_morphism f r r'->
injection f.
Proof.
move => [or or' [ff sf tf] h].
split => // x y xsf ysf sv.
have aux: gle r' (Vf f y) (Vf f y) by order_tac; Wtac.
apply: (order_antisymmetry or).
apply/(h _ _ xsf ysf); ue.
apply/(h _ _ ysf xsf); ue.
Qed.

Lemma order_isomorphism_w r r' f:
order_isomorphism f r r' -> order_morphism f r r'.
Proof. by move=> [or or' [ [[ff _] _] sf tf] etc]. Qed.

Lemma order_isomorphism_ws r r' f:
bijection f -> order_morphism f r r' -> order_isomorphism f r r'.
Proof. by move=> bf [or or'[ _ sf tf] etc]. Qed.

Lemma order_morphism_incr f r r': order_morphism f r r' -> fincr_prop f r r'.
Proof.
move => [or or' [ff sf tf] h] x y rxy.
have xsr: inc x (source f) by rewrite sf; order_tac.
have ysr: inc y (source f) by rewrite sf; order_tac.
by move/(h _ _ xsr ysr):rxy.
Qed.

Lemma order_isomorphism_incr f r r':
order_isomorphism f r r' -> fincr_prop f r r'.
Proof.
by move => h; apply: order_morphism_incr; apply:order_isomorphism_w.
Qed.

Lemma order_morphism_sincr f r r': order_morphism f r r' -> fsincr_prop f r r'.
Proof.
move => h; move: (order_morphism_fi h) => fi.
move: h => [or or' [ff sf tf] h] x y [rxy nxy].
have xsr: inc x (source f) by rewrite sf; order_tac.
have ysr: inc y (source f) by rewrite sf; order_tac.
split; first by move/(h _ _ xsr ysr):rxy.
by dneg aux; apply: (proj2 fi).
Qed.

Lemma order_isomorphism_sincr f r r':
order_isomorphism f r r' -> fsincr_prop f r r'.
Proof.
by move => h; apply: order_morphism_sincr; apply:order_isomorphism_w.
Qed.

Lemma order_morphism_siso f r r': order_morphism f r r' -> fsiso_prop f r r'.
Proof.
move => h x y xsf ysf; split; first by apply :order_morphism_sincr.
move: (order_morphism_fi h) => fi.
move: h => [or or' [ff sf tf] h].
by move => [pa pb]; split; [ apply /h | move => h1; case: pb; rewrite h1].
Qed.

Lemma order_isomorphism_siso f r r': order_isomorphism f r r'
-> fsiso_prop f r r'.
Proof.
by move => h; apply: order_morphism_siso; apply:order_isomorphism_w.
Qed.

Lemma identity_is r: order r ->
order_isomorphism (identity (substrate r)) r r.
Proof.
move=> or; red; rewrite /fiso_prop; aw; split => //.
split; aw;apply: identity_fb.
move=> x t xsr ysr;rewrite ? identity_V //.
Qed.

Lemma identity_morphism r: order r ->
order_morphism (identity (substrate r)) r r.
Proof.
by move=> or; apply: order_isomorphism_w; apply: identity_is.
Qed.

Lemma compose_order_morphism r r' r'' f f':
order_morphism f r r' -> order_morphism f' r' r''
-> order_morphism (f' \co f) r r''.
Proof.
move=>[or or' [ff sf tf] fp][_ or'' [ff' sf' tf'] fp'].
have cff': f' \coP f by split => // ; rewrite sf'.
split => //; first by split; aw; fct_tac.
red; aw; move=> x y xsf ysf; aw.
move: (Vf_target ff xsf)(Vf_target ff ysf); rewrite tf - sf' => xt yt.
split; first by move => h; apply /(fp' _ _ xt yt) /(fp _ _ xsf ysf).
by move/(fp' _ _ xt yt) /(fp _ _ xsf ysf).
Qed.

Lemma compose_order_is r r' r'' f f':
order_isomorphism f r r' -> order_isomorphism f' r' r''
-> order_isomorphism (f' \co f) r r''.
Proof.
move => pa pb;
move: (order_isomorphism_w pa) (order_isomorphism_w pb) => h1 h2.
apply: order_isomorphism_ws (compose_order_morphism h1 h2).
move: pa pb =>[_ _ [bf sf tf] _][_ _ [bf' sf' tf'] _].
by apply: compose_fb => //; split => // ; try fct_tac; rewrite sf'.
Qed.

Lemma inverse_order_is r r' f:
order_isomorphism f r r' -> order_isomorphism (inverse_fun f) r' r.
Proof.
rewrite /order_isomorphism.
move=>[or or' [bf sf tf] fp];split =>//; aw.
by split => //; aw; apply: inverse_bij_fb.
move=> x y xt yt.
move: (xt)(yt); aw => xt1 yt1.
rewrite -{1} (inverse_V bf xt1) -{1} (inverse_V bf yt1).
have aux: (source f = target (inverse_fun f)) by aw.
move: (inverse_bij_fb bf) => [[fi _] _].
symmetry;apply/fp; rewrite aux; Wtac.
Qed.

Lemma orderIR r: order r -> r \Is r.
Proof. by move=> or; exists (identity (substrate r)); apply: identity_is. Qed.

Lemma orderIS r r': r \Is r' -> r' \Is r.
Proof.
move=> [f fi]; exists (inverse_fun f); apply: (inverse_order_is fi).
Qed.

Lemma orderIT r' r r'': r \Is r' -> r' \Is r'' -> r \Is r''.
Proof.
move=> [f oif][g oig]; exists (g \co f); apply: (compose_order_is oif oig).
Qed.

## Ordered subsets. Product of ordered sets

Order induced by r on a

Definition induced_order r a := r \cap (coarse a).

Lemma iorder_gle5P r a x y:
gle (induced_order r a) x y <-> [/\ inc x a, inc y a & gle r x y].
Proof.
split; first by move/setI2_P => [h /setXp_P [pa pb]].
by move => [pa pb pc]; apply /setI2_i => //;apply/setXp_P.
Qed.

Lemma iorder_gle6P r a x y:
glt (induced_order r a) x y <-> [/\ inc x a, inc y a & glt r x y].
Proof.
split; first by move => [] /iorder_gle5P [pa pb pc] pd.
by move => [pa pb [pc pd]]; split => //; apply /iorder_gle5P.
Qed.

Lemma iorder_gleP r a x y: inc x a -> inc y a ->
(gle (induced_order r a) x y <-> gle r x y).
Proof.
move=> xa ya;split;first by move/iorder_gle5P => [_ _].
by move => pa; apply /iorder_gle5P.
Qed.

Lemma iorder_gle1 r a x y:
gle (induced_order r a) x y -> gle r x y.
Proof. by move/iorder_gle5P=> [_ _]. Qed.

Lemma iorder_gle2 r a x y:
glt (induced_order r a) x y -> glt r x y.
Proof. by move/iorder_gle6P=> [_ _]. Qed.

Lemma iorder_gle3 r a x y:
gle (induced_order r a) x y -> (inc x a /\ inc y a).
Proof. by move/iorder_gle5P=> [pa pb _]. Qed.

Lemma iorder_gle4 r a x y:
glt (induced_order r a) x y -> (inc x a /\ inc y a).
Proof. by move/iorder_gle6P=> [pa pb _]. Qed.

Lemma iorder_preorder r a:
sub a (substrate r) ->
preorder r -> preorder (induced_order r a).
Proof.
move=> ar [gr rr tr];red.
have gi: sgraph (induced_order r a) by apply: (setI2_graph1 gr (y:=coarse a)).
split => //.
move => t ti.
have ta: inc t a.
by move: ti => /(substrate_P gi) [] [y]/iorder_gle5P [ta tb _].
by apply /iorder_gle5P;split => //;apply: rr; apply: ar.
move=> x y z /iorder_gle5P [xa ya rxy] /iorder_gle5P [_ za ryz].
apply/iorder_gle5P;split => //; apply: tr rxy ryz.
Qed.

Lemma iorder_osr r a: order r ->sub a (substrate r)
-> order_on (induced_order r a) a.
Proof.
move=> ar or.
have: preorder (induced_order r a).
by apply: iorder_preorder =>//; apply: order_preorder.
move=> [go rio tio]; split.
split => // x y /iorder_gle5P [_ _ rxy] /iorder_gle5P [_ _ ryz]; order_tac.
set_extens t.
by move/(substrate_P go) => [] [y] /iorder_gle5P [pa pb _].
move => ta; move: (or _ ta) => tb.
by apply /(substrate_P go); left; exists t; apply /iorder_gleP => //;order_tac.
Qed.

Lemma iorder_sr r a: order r ->sub a (substrate r)
-> substrate (induced_order r a) = a.
Proof. move => pa pb; exact (proj2 (iorder_osr pa pb)). Qed.

Hint Rewrite iorder_sr: aw.

Lemma iorder_substrate r:
order r -> induced_order r (substrate r) = r.
Proof.
move=> o;apply/setI2id_Pl;apply: sub_graph_coarse_substrate; fprops.
Qed.

Lemma iorder_trans a b c: sub c b ->
induced_order (induced_order a b) c = induced_order a c.
Proof.
move=> cb; rewrite /induced_order.
have scc: (sub (coarse c) (coarse b)) by apply:setX_Sll.
by rewrite - setI2_A; congr ( a \cap _); apply/setI2id_Pr.
Qed.

Lemma iorder_opposite r x: order r ->
commutes_at (induced_order ^~ x) (opp_order) r.
Proof.
move => or.
apply: sgraph_exten.
apply: (setI2_graph2); apply: coarse_graph.
apply: igraph_graph.
move => u v; split.
move /iorder_gle5P => [pa pb /igraph_pP pc].
by apply/igraph_pP; apply /iorder_gle5P.
move/igraph_pP => /iorder_gle5P [pa pb pc].
by apply /iorder_gle5P;split => //; apply /igraph_pP.
Qed.

Example 1. The function that associates to a partial function its graph. Is an isomorphism for extends and inclusion

Definition fgraphs x y :=
Zo (powerset (x \times y)) fgraph.

Definition graph_of_function x y :=
Lf graph (sub_functions x y) (fgraphs x y).

Lemma graph_of_function_sub x y z:
inc z (sub_functions x y) -> sub (graph z) (x \times y).
Proof.
move /sfun_set_P=> [[[_ p] _ _] sz <-].
by apply: (sub_trans p); apply:setX_Slr.
Qed.

Lemma set_of_graphs_pr x y z:
inc z (sub_functions x y) -> inc (graph z) (fgraphs x y).
Proof.
move=> zs; apply: Zo_i; first by apply/setP_P;apply: graph_of_function_sub.
by move /sfun_set_P: zs => [[cz fz _] _ _].
Qed.

Lemma graph_of_function_f x y:
function (graph_of_function x y).
Proof.
by apply: lf_function; apply: set_of_graphs_pr.
Qed.

Lemma graph_of_function_V x y f:
inc f (sub_functions x y) -> Vf (graph_of_function x y) f = graph f.
Proof.
by rewrite /graph_of_function=> fs; aw; apply: set_of_graphs_pr.
Qed.

Lemma graph_of_function_fb x y:
bijection (graph_of_function x y).
Proof.
rewrite /graph_of_function.
apply: lf_bijective.
by apply: set_of_graphs_pr.
move=> u v /sfun_set_P [fu ssu tu] /sfun_set_P [fv sv tv] sg.
by apply: function_exten1=>//; ue.
move=> z /Zo_P [] /setP_P zp fx.
move: (sub_setX_graph zp) => gz.
exists (triple (domain z) y z); aw; apply/sfun_set_P;split; aw.
apply: function_pr => //.
by move => t /(rangeP gz) [u Jz]; move: (zp _ Jz) => /setXp_P [].
by move => t /(domainP gz) [u Jz]; move: (zp _ Jz) => /setXp_P [].
Qed.

Lemma graph_of_function_is x y:
order_isomorphism (graph_of_function x y)
(opp_order (extension_order x y))
(sub_order (fgraphs x y)).
Proof.
move: (extension_osr x y) => [eo sr].
move:(sub_osr (fgraphs x y)) => [sio sis].
move: (opp_osr eo) => [ex sx].
red; rewrite /fiso_prop sis sx sr.
have <- :sub_functions x y = source (graph_of_function x y).
rewrite /graph_of_function; aw.
split; fprops.
rewrite /graph_of_function. split; aw => //.
by apply: graph_of_function_fb.
move=> a b ass bss.
rewrite graph_of_function_V // graph_of_function_V //.
split.
move /extension_order_P2 => [_ _ h]; apply/sub_gleP.
by split => //; apply: set_of_graphs_pr.
by move /sub_gleP => [pa pb pc]; apply /extension_order_P2.
Qed.

Example 2. The mapping that associates to a partition the graph of the equivalence is an order isomorphism onto its image

Definition graph_of_partition x :=
Lf (fun y => partition_relset y x)
(partitions x)(powerset (coarse x)).

Lemma gop_axioms x:
lf_axiom (fun y => partition_relset y x)
(partitions x) (powerset (coarse x)).
Proof.
move=> y /partitionsP => h; apply/setP_P.
by apply: sub_part_relsetX.
Qed.

Lemma gop_V x y:
partition_s y x ->
Vf (graph_of_partition x) y = partition_relset y x.
Proof.
rewrite /graph_of_partition=> pa; aw; first by apply: gop_axioms.
by apply /partitionsP.
Qed.

Lemma gop_morphism x:
order_morphism (graph_of_partition x) (coarser x)
(opp_order (subp_order (coarse x))).
Proof.
move:(sub_osr (coarse x)) => [oi sr].
move:(coarser_osr x) => [oc sr'].
move:(subp_osr (coarse x)) => [pa1 pb1].
move: (opp_osr pa1) => [pa2 pb2].
have gi: (sgraph (sub_order (coarse x))) by fprops.
have sg: source (graph_of_partition x) = (partitions x).
by rewrite /graph_of_partition; aw.
split;fprops.
split; rewrite ? pb2 ? pb1 ? sr' /graph_of_partition;aw.
by apply: lf_function; apply: gop_axioms.
move => a b.
rewrite sg; move /partitionsP => pa /partitionsP pb.
rewrite - partition_relset_order // gop_V // gop_V //.
split; last by move/igraph_pP => /sub_gleP [_ _].
move => h; apply/igraph_pP; apply /sub_gleP.
by split => //; apply /setP_P /sub_part_relsetX.
Qed.

Example 3: Compare preorder relations

Definition preorder_on r E := preorder r /\ substrate r = E.
Definition preorders x :=
Zo (powerset (coarse x))(preorder_on ^~ x).

Lemma preordersP x z:
inc z (preorders x) <-> (preorder_on z x).
Proof.
split; first by move/Zo_P => [].
move => h;apply:Zo_i => //;apply/setP_P.
move: h => [pa pb]; rewrite -pb; apply:sub_graph_coarse_substrate.
by apply: preorder_sgraph.
Qed.

Definition coarser_preorder x := sub_order (preorders x).

Lemma coarser_preorder_osr x:
order_on (coarser_preorder x) (preorders x).
Proof. exact: sub_osr. Qed.

Lemma coarser_preorder_gleP x u v:
gle (coarser_preorder x) u v <->
[/\ preorder u, preorder v, substrate u = x, substrate v = x & sub u v].
Proof.
split; first by move/sub_gleP => [] /Zo_hi [xa pa] /Zo_hi [ya pb] pc.
move => [pa pb pc pd pe]; apply /sub_gleP.
by split => //; apply /preordersP.
Qed.

Lemma coarser_preorder_gleP1 x u v:
gle (coarser_preorder x) u v <->
[/\ preorder u, preorder v, substrate u = x, substrate v = x &
forall a b, inc a x -> inc b x -> related u a b -> related v a b].
Proof.
split.
move/coarser_preorder_gleP => [pu pv su sv hyp]; split => //.
by move=> a b ax bx J1; apply: hyp.
move => [pu pv su sv hyp].
apply /coarser_preorder_gleP; split => // t tu.
move: (preorder_sgraph pu tu) => p.
rewrite -p in tu |- *; apply: hyp =>//; rewrite - su; substr_tac.
Qed.

If g is a family of orders, we consider f the family of susbtrates. We consider here the ordering induced by g on the product of f

Definition fam_of_substrates g :=
Lg (domain g) (fun i => substrate (Vg g i)).

Definition prod_of_substrates g := productb (fam_of_substrates g).

Definition order_fam g := allf g order.

Definition order_product_r g x x' :=
forall i, inc i (domain g) -> gle (Vg g i) (Vg x i) (Vg x' i).

Definition order_product g :=
graph_on (order_product_r g)(prod_of_substrates g).

Lemma fos_graph f: fgraph (fam_of_substrates f).
Proof. rewrite /fam_of_substrates; fprops. Qed.

Lemma fos_d f: domain (fam_of_substrates f) = domain f.
Proof. rewrite /fam_of_substrates; bw. Qed.

Lemma fos_V f x: inc x (domain f) ->
Vg (fam_of_substrates f) x = substrate (Vg f x).
Proof. move => xdf; rewrite /fam_of_substrates; bw. Qed.

Hint Rewrite fos_d fos_V : bw.

Lemma prod_of_substratesP g x:
inc x (prod_of_substrates g) <->
[/\ fgraph x, domain x = domain g &
forall i, inc i (domain g) -> inc (Vg x i) (substrate (Vg g i))].
Proof.
split.
move/setXb_P; bw; move=> [fgx dx asu];split => //.
move => i idg; move: (asu _ idg); bw.
move => [pa pb pc]; apply /setXb_P; bw;split=> //.
move => i idg; move: (pc _ idg); bw.
Qed.

Lemma prod_of_substrates_p g x i:
inc x (prod_of_substrates g) ->
inc i (domain g) -> inc (Vg x i) (substrate (Vg g i)).
Proof. move =>/(prod_of_substratesP) [_ _]; apply. Qed.

Lemma prod_of_substrates_gi g f:
(forall i, inc i (domain g) -> inc (f i) (substrate (Vg g i))) ->
inc (Lg (domain g) f) (prod_of_substrates g).
Proof.
move => pb; apply/(prod_of_substratesP);split => //; fprops; bw.
by move => i idg; bw; apply: pb.
Qed.

Lemma order_product_gleP g x x':
(gle (order_product g) x x' <->
[/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) &
forall i, inc i (domain g) -> gle (Vg g i) (Vg x i)(Vg x' i)]).
Proof. apply /graph_on_P0. Qed.

Lemma order_product_osr g:
order_fam g -> order_on (order_product g) (prod_of_substrates g).
Proof.
move=> poa; move: (poa) => oa; split.
rewrite /order_product/order_product_r.
apply: order_from_rel1.
- move=> /= x y z pxy pyz i idg.
move: (pxy _ idg) (pyz _ idg)(oa _ idg) => *; order_tac.
- move=> x y; rewrite /prod_of_substrates => xp yp p1 p2.
apply: (setXb_exten xp yp); bw.
move=> i idg; move: (p2 _ idg) (p1 _ idg)(oa _ idg)=> *; order_tac.
- move=> u up i idg; move: (oa _ idg) => oi.
by order_tac; apply: prod_of_substrates_p.
apply: graph_on_sr.
move => a ap i idg; move: (poa _ idg) => oi.
by order_tac; apply:prod_of_substrates_p.
Qed.

Let g be a family of orders, f the family of substrates, p the product of f and r the product order of the family g; its substrate is p. There a canonical bijection from product p p onto the product of all product (f i) (f i). The bijection maps r to the product of g

Lemma product_order_def g (f := fam_of_substrates g):
order_fam g ->
image_by_fun (prod_of_products_canon f f) (order_product g) = (productb g).
Proof.
set opg:= order_product g => oa.
have dfdg: domain f = domain g by rewrite /f; bw.
set (F:= triple (domain f) (range f) f).
have ff: fgraph f by apply: fos_graph.
have fF: function F by rewrite /F; apply: function_pr;fprops.
have gF: graph F = f by rewrite /F; aw.
have fp: function (prod_of_products_canon f f).
move: (popc_fb fF fF (refl_equal (source F))); rewrite gF=> h; fct_tac.
move:(order_product_osr oa) => [xx poo].
have spgs: sub opg (source (prod_of_products_canon f f)).
rewrite /prod_of_products_canon; aw.
have gpo: sgraph opg by fprops.
by move: (sub_graph_coarse_substrate gpo); rewrite poo.
set_extens x.
move /(Vf_image_P fp spgs) => [u upo].
move: (spgs _ upo); rewrite {1} /prod_of_products_canon lf_source -gF => upob.
rewrite popc_V //; move => ->.
move: upob; rewrite gF.
move /setX_P => [pu /setXb_P [fgP dPu alp]].
move => /setXb_P [fgQ dQu alq]; apply /setXb_P.
rewrite /prod_of_fgraph;split; bw; fprops.
by rewrite dPu dfdg.
move=> i idg; bw; last by rewrite dPu dfdg.
have: (gle opg (P u) (Q u)) by red; red; rewrite pu.
move /(order_product_gleP) => [_ _ h]; move: (h _ idg) => wp; aw.
set x1:= Lg (domain g) (fun i => P (Vg x i)).
set x2:= Lg (domain g) (fun i => Q (Vg x i)).
move/setXb_P => [fgx dxdg idx].
have p1: inc x1 (prod_of_substrates g).
by apply: (prod_of_substrates_gi) => // i idg; apply: pr1_sr; apply: idx.
have p2: inc x2 (prod_of_substrates g).
by apply: (prod_of_substrates_gi) => // i idg; apply: pr2_sr; apply: idx.
have p3: forall i, inc i (domain g) -> pairp (Vg x i).
move=> i idg; apply: (order_sgraph (oa _ idg) (idx _ idg)).
apply/(Vf_image_P fp spgs); exists (J x1 x2).
apply/(order_product_gleP);split => // i idg.
by rewrite/x1/x2; bw; red; red;rewrite (p3 _ idg); apply: idx.
rewrite -gF popc_V //.
symmetry.
aw; rewrite /prod_of_fgraph /x1 /x2; apply:fgraph_exten=> //; bw; fprops.
by move => i idg /=; bw; apply: p3.
by rewrite gF; apply: setXp_i.
Qed.

Special case of a product of 2 orders

Definition order_product2 f g := prod_of_relation f g.

Lemma order_product2_P f g x x':
gle (order_product2 f g) x x' <->
[/\ inc x ((substrate f) \times (substrate g)),
inc x' ((substrate f)\times (substrate g)) &
gle f (P x) (P x') /\ gle g (Q x) (Q x')].
Proof.
split; first by move/Zo_P =>[] /setXp_P; aw; move => [pa pb] pc.
move => [pa pb pc]; apply: Zo_i; [ by apply:setXp_i | aw ].
Qed.

Order on graphs of functions x->y, induced by an order g on the target. This is a special case of product order.

Definition order_graph_r x r z z' :=
forall i, inc i x -> gle r (Vg z i) (Vg z' i).

Definition order_graph x y r :=
graph_on (order_graph_r x r) (gfunctions x y).

Lemma order_fam_cst x r: order r -> order_fam (cst_graph x r).
Proof. rewrite /cst_graph=> og; move; bw; move=> i id; bw. Qed.

Lemma order_graph_r_P x r z z':
order_graph_r x r z z' <->
order_product_r (cst_graph x r) z z'.
Proof.
have dc: (domain (cst_graph x r) = x) by bw.
rewrite /order_product_r dc /cst_graph.
split; first by move=> go i ix; bw; apply: go.
move=> h y yx; move: (h _ yx); bw.
Qed.

Section OrderGraph.
Variables (x y g: Set).
Hypothesis (sr: substrate g = y).

Lemma order_graph_pr1:
(gfunctions x y) = prod_of_substrates (cst_graph x g).
Proof.
rewrite -cst_graph_pr /prod_of_substrates /fam_of_substrates /cst_graph.
bw; rewrite - sr; congr (productb _); apply: Lg_exten; move=> v vs /=; bw.
Qed.

Lemma order_graph_pr:
order_graph x y g = order_product (cst_graph x g).
Proof.
rewrite /order_graph/order_product (order_graph_pr1) {2}/cst_graph.
rewrite /graph_on/order_product_r Lg_domain.
set_extens t => /Zo_P [t1 h]; apply /Zo_P;split =>// i ix; move: (h _ ix); bw.
Qed.

Lemma order_graph_osr: order g ->
order_on (order_graph x y g) (gfunctions x y).
Proof.
move=> og ; rewrite order_graph_pr =>//.
move:(order_product_osr (order_fam_cst og (x:=x))) => [pa pb].
by split => //; rewrite (order_graph_pr1).
Qed.

End OrderGraph.

Order on functions x->y, induced by an order r on the target

Definition order_function_r x y r f g :=
[/\ function_prop f x y, function_prop g x y &
forall i, inc i x -> gle r (Vf f i) (Vf g i)].

Definition order_function x y r :=
graph_on (order_function_r x y r) (functions x y).

Section OrderFunction.
Variables (x y r: Set).
Hypothesis (or: order r) (sr: substrate r = y).

Lemma order_functionP f f':
gle (order_function x y r) f f' <->
[/\ inc f (functions x y),
inc f' (functions x y) &
forall i, inc i x -> gle r (Vf f i) (Vf f' i)].
Proof.
split.
by move /Zo_P => [/setXp_P [pa pb]]; aw; move => [_ _ bb].
move => [pa pb pc];apply:Zo_i; first by apply:setXp_i.
move/fun_set_P: pa => pa.
move/fun_set_P: pb => pb.
by red; aw.
Qed.

Lemma order_function_osr: order_on (order_function x y r)(functions x y).
Proof.
have gf: sgraph (order_function x y r) by apply: graph_on_graph.
have rr:forall u, inc u (functions x y) -> gle (order_function x y r) u u.
move=> u us; apply: Zo_i; rewrite /coarse;fprops.
aw; move /fun_set_P: us => [fu su tu].
red; split => // i ix; order_tac.
rewrite sr -tu; rewrite - su in ix; fprops.
have sr1: substrate (order_function x y r) = functions x y.
set_extens t.
by case/(substrate_P gf) => [] [z] /Zo_P [] /setXp_P [].
by move=> ts; apply: substr_i; apply: rr.
split => //; split.
rewrite /order_function;apply: graph_on_graph.
move=> z zs; apply: rr;rewrite - sr1 //.
move=> a b c/order_functionP [afs bfs leab] /order_functionP [_ cfs lebc].
apply/order_functionP;split=> //.
move=> i id; move: (leab _ id) (lebc _ id) => lab lbc; order_tac.
move=> a b /order_functionP [afs bfs leab] /order_functionP [_ _ leba].
move: afs bfs => /fun_set_P [fa sa ta] /fun_set_P [fb sb tb].
apply: function_exten=>//; try ue.
rewrite sa; move=> i ix;move: (leab _ ix) (leba _ ix)=> lab lba; order_tac.
Qed.

The mapping that associates to a function its graph is an isomorphism for the two orders defined above

Lemma order_function_is:
order_isomorphism (Lf graph (functions x y)(gfunctions x y))
(order_function x y r)(order_graph x y r).
Proof.
move: order_function_osr => [pa pb].
move: (order_graph_osr x sr or)=> [pc pd].
split => //.
split; aw => //;apply: graph_fb.
red;move: (graph_lf_axiom (x:=x) (y:=y))=> ax; aw=> a b ass bss; aw.
split.
move/order_functionP => [_ _ h];apply:Zo_i;aw;by apply:setXp_i; apply: ax.
by move /Zo_hi;aw => xx; apply/order_functionP.
Qed.

Lemma order_function_is1: (order_function x y r) \Is (order_graph x y r).
Proof.
exists (Lf graph (functions x y) (gfunctions x y)).
by apply: order_function_is.
Qed.

End OrderFunction.

## Increasing mappings

Definition increasing_fun f r r' :=
[/\ order r, order r', function_prop f (substrate r) (substrate r')
& fincr_prop f r r'].

Definition decreasing_fun f r r' :=
[/\ order r, order r', function_prop f (substrate r) (substrate r')
& forall x y, gle r x y -> gle r' (Vf f y) (Vf f x)].

Definition monotone_fun f r r' :=
increasing_fun f r r' \/ decreasing_fun f r r'.

Monotonicity and opposite order

Lemma increasing_fun_reva f r r':
increasing_fun f r r' -> decreasing_fun f r (opp_order r').
Proof.
rewrite /increasing_fun/decreasing_fun=> [] [or or' [ff sr sr'] rel].
move: (opp_osr or') => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y xy; apply/igraph_pP; apply: rel.
Qed.

Lemma increasing_fun_revb f r r':
increasing_fun f r r' -> decreasing_fun f (opp_order r) r'.
Proof.
rewrite /increasing_fun/decreasing_fun=> [] [or or' [ff sr sr'] rel].
move: (opp_osr or) => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y /igraph_pP => xy;apply: rel.
Qed.

Lemma decreasing_fun_reva f r r':
decreasing_fun f r r' -> increasing_fun f r (opp_order r').
Proof.
rewrite /increasing_fun/decreasing_fun=> [] [or or' [ff sr sr'] rel].
move: (opp_osr or') => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y xy; apply/igraph_pP; apply: rel.
Qed.

Lemma decreasing_fun_revb f r r':
decreasing_fun f r r' -> increasing_fun f (opp_order r) r'.
Proof.
rewrite /increasing_fun/decreasing_fun=> [] [or or' [ff sr sr'] rel].
move: (opp_osr or) => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y /igraph_pP => xy;apply: rel.
Qed.

Lemma monotone_fun_reva f r r':
monotone_fun f r r' -> monotone_fun f r (opp_order r').
Proof.
rewrite /monotone_fun; case.
by right; apply: increasing_fun_reva.
by left; apply: decreasing_fun_reva.
Qed.

Lemma monotone_fun_revb f r r':
monotone_fun f r r' -> monotone_fun f (opp_order r) r'.
Proof.
rewrite /monotone_fun; case.
by right; apply: increasing_fun_revb.
by left; apply: decreasing_fun_revb.
Qed.

Strict monotone functions

Definition strict_increasing_fun f r r' :=
[/\ order r, order r',function_prop f (substrate r) (substrate r')
& fsincr_prop f r r'].
Definition strict_decreasing_fun f r r' :=
[/\ order r, order r',function_prop f (substrate r) (substrate r')
& forall x y, glt r x y -> glt r' (Vf f y) (Vf f x)].

Definition strict_monotone_fun f r r' :=
strict_increasing_fun f r r' \/ strict_decreasing_fun f r r'.

Lemma strict_increasing_fun_reva f r r':
strict_increasing_fun f r r' -> strict_decreasing_fun f r (opp_order r').
Proof.
rewrite/ strict_increasing_fun/strict_decreasing_fun.
move=> [or or' [ ff sr sr'] rel].
move: (opp_osr or') => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y xy;apply /opp_gltP; apply: rel.
Qed.

Lemma strict_increasing_fun_revb f r r':
strict_increasing_fun f r r' -> strict_decreasing_fun f (opp_order r) r'.
Proof.
rewrite/ strict_increasing_fun/strict_decreasing_fun.
move=> [or or' [ ff sr sr'] rel].
move: (opp_osr or) => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y /opp_gltP;apply: rel.
Qed.

Lemma strict_decreasing_fun_reva f r r':
strict_decreasing_fun f r r' -> strict_increasing_fun f r (opp_order r').
Proof.
rewrite/ strict_increasing_fun/strict_decreasing_fun.
move=> [or or' [ ff sr sr'] rel].
move: (opp_osr or') => [pa pb]; split => //; first by split; aw;rewrite pb.
by move=> x y xy; apply /opp_gltP; apply: rel.
Qed.

Lemma strict_decreasing_fun_revb f r r':
strict_decreasing_fun f r r' -> strict_increasing_fun f (opp_order r) r'.
Proof.
rewrite/ strict_increasing_fun/strict_decreasing_fun.
move=> [or or' [ ff sr sr'] rel].
move: (opp_osr or) => [pa pb]; split => //; first by split; aw;rewrite pb.
move=> x y /opp_gltP; apply: rel.
Qed.

Lemma strict_monotone_fun_reva f r r':
strict_monotone_fun f r r' -> strict_monotone_fun f r (opp_order r').
Proof.
rewrite /strict_monotone_fun; case.
by right; apply: strict_increasing_fun_reva.
by left; apply: strict_decreasing_fun_reva.
Qed.

Lemma strict_monotone_fun_revb f r r':
strict_monotone_fun f r r' -> strict_monotone_fun f (opp_order r) r'.
Proof.
rewrite /strict_monotone_fun; case.
by right; apply: strict_increasing_fun_revb.
by left; apply: strict_decreasing_fun_revb.
Qed.

Lemma strict_increasing_w f r r':
strict_increasing_fun f r r' -> increasing_fun f r r'.
Proof.
move=> [or or' [ ff sr sr'] rel]; split => //.
move => x y h; case: (equal_or_not x y) => xy.
rewrite - xy; order_tac; rewrite - sr'; Wtac; rewrite sr; order_tac.
exact: (proj1 (rel _ _ (conj h xy))).
Qed.

Lemma strict_decreasing_w f r r':
strict_decreasing_fun f r r' -> decreasing_fun f r r'.
Proof.
move=> [or or' [ ff sr sr'] rel]; split => //.
move => x y h; case: (equal_or_not x y) => xy.
rewrite - xy; order_tac; rewrite - sr'; Wtac; rewrite sr; order_tac.
exact: (proj1 (rel _ _ (conj h xy))).
Qed.

Lemma order_morphism_increasing f r r':
order_morphism f r r' ->
strict_increasing_fun f r r'.
Proof.
move => h; move: (order_morphism_sincr h) => si.
move:h=> [or or' [ ff sr sr'] rel]; split => //.
Qed.

Lemma order_isomorphism_increasing f r r':
order_isomorphism f r r' ->
strict_increasing_fun f r r'.
Proof.
move => h; apply order_morphism_increasing.
by apply order_isomorphism_w.
Qed.

Example of monotone functions.

Lemma constant_fun_increasing f r r':
order r -> order r' -> substrate r = source f ->
substrate r' = target f -> constantfp f ->
increasing_fun f r r'.
Proof.
move=> or or' sr sr' [ff cf].
split => //.
move=> x y rxy.
have xs: (inc x (source f)) by rewrite - sr; order_tac.
have ys: (inc y (source f)) by rewrite - sr;order_tac.
rewrite (cf _ _ xs ys); order_tac; ue.
Qed.

Lemma constant_fun_decreasing f r r':
order r -> order r' -> substrate r = source f ->
substrate r' = target f -> constantfp f ->
decreasing_fun f r r'.
Proof.
move=> or or' sr sr' [ff cf].
split => //.
move=> x y rxy.
have xs: (inc x (source f)) by rewrite - sr;order_tac.
have ys: (inc y (source f)) by rewrite - sr;order_tac.
rewrite (cf _ _ xs ys); order_tac; ue.
Qed.

Lemma identity_increasing_decreasing x (r := diagonal x) :
(increasing_fun (identity x) r r /\ decreasing_fun (identity x) r r).
Proof.
move: (diagonal_osr x) => [oi si].
have pa: function_prop (identity x) (substrate r) (substrate r).
red; aw; split => //; apply:(identity_f x).
split;split => //.
move=> a b rab; bw; rewrite - si; order_tac.
move=> a b rab; bw; try (rewrite - si; order_tac).
by move: rab => /diagonal_pi_P [ax] <-; apply/diagonal_pi_P.
Qed.

Lemma setC_decreasing E:
strict_decreasing_fun (Lf (complement E)(powerset E)(powerset E))
(subp_order E) (subp_order E).
Proof.
move: (subp_osr E); set (r:=sub_order E); move => [or sr].
have ta: lf_axiom (complement E) (powerset E) (powerset E).
move=> c cE;apply/setP_P; apply: sub_setC.
split => //; first by red; aw; split => //; apply: lf_function.
move=> x y [] /subp_gleP [xE yE xy] nxy.
aw; try (apply/setP_P => //); split.
apply/subp_gleP;split; try (apply:sub_setC); by apply /(set_CSm xE yE).
dneg cc; move:(f_equal (complement E) cc).
by rewrite (setC_K yE) (setC_K xE).
Qed.

If M x is the set of upper bounds of x then M is striclty decreasing in the power set

Definition set_of_upper_bounds1 r x :=
Zo (substrate r)(fun y => gle r x y).

Lemma set_of_upper_bounds1_P x y r:
order r -> inc x (substrate r) -> inc y (substrate r) ->
(gle r x y <-> sub (set_of_upper_bounds1 r y) (set_of_upper_bounds1 r x)).
Proof.
rewrite /set_of_upper_bounds1 => or xs ys;split.
move=> lexy t /Zo_P [ts yt]; apply :Zo_i => //;order_tac.
set s:= Zo _ _; move=> ss.
have yss: inc y s by rewrite /s Zo_P; split => //; order_tac.
by move /Zo_P: (ss _ yss)=> [].
Qed.

Lemma set_of_upper_bounds1_decreasing r:
order r ->
strict_decreasing_fun
(Lf (set_of_upper_bounds1 r) (substrate r)(powerset (substrate r)))
r (subp_order (substrate r)).
Proof.
move=> or; red; bw; aw.
set E:= substrate r.
move:(subp_osr E) => [oe si].
have ta: lf_axiom (set_of_upper_bounds1 r) E (powerset E).
by move=> x xE; apply /setP_P => t /Zo_P [].
split => //.
by rewrite si;split; aw; apply: lf_function.
move => x y ltxy.
have xE: inc x E by rewrite /E;order_tac.
have yE: inc y E by rewrite /E;order_tac.
move: ltxy=> [lexy nxy].
move:(lexy) => /(set_of_upper_bounds1_P or xE yE) => sxy.
aw; split.
apply /subp_gleP;split => //.
by move: (ta _ yE) =>/setP_P.
by move: (ta _ xE) =>/setP_P.
dneg seq.
suff: gle r y x by move => le; order_tac.
by apply/(set_of_upper_bounds1_P or yE xE) ;rewrite seq; fprops.
Qed.

comparison of monotone and morphism

Lemma strict_increasing_from_injective f r r':
injection f -> increasing_fun f r r' -> strict_increasing_fun f r r'.
Proof.
move=> [_ inf] [or or' [ ff sr sr'] rel]; split => //.
move=> x y [lexy neq]; split; first by apply: rel.
dneg Wxy; apply: inf=>//; rewrite sr; order_tac.
Qed.

Lemma strict_decreasing_from_injective f r r':
injection f -> decreasing_fun f r r' -> strict_decreasing_fun f r r'.
Proof.
move=> [_ inf] [or or' [ ff sr sr'] rel]; split => //.
move=> x y [lexy neq]; split; first by apply: rel.
dneg Wxy; apply: inf=>//; rewrite sr; order_tac.
Qed.

Lemma strict_monotone_from_injective f r r':
injection f -> monotone_fun f r r' -> strict_monotone_fun f r r'.
Proof.
move=> inf; case.
by left; apply: strict_increasing_from_injective.
by right; apply: strict_decreasing_from_injective.
Qed.

Lemma order_isomorphism_P f r r':
order r -> order r' ->
bijection f -> substrate r = source f -> substrate r' = target f ->
(order_isomorphism f r r' <->
(increasing_fun f r r' /\ increasing_fun (inverse_fun f) r' r)).
Proof.
move=> or or' bf sr sr'.
move: (bijective_inv_f bf)=> bif.
have sf: source f = target (inverse_fun f) by rewrite /inverse_fun; aw.
have tf: target f = source (inverse_fun f) by rewrite /inverse_fun; aw.
split.
move => h; move:(order_isomorphism_incr h) => h2.
move: h => [_ _ _ h1].
split; split;aw.
- split=> //; fct_tac.
- split;aw => //; fct_tac.
- move=>x y rxy.
have xt: inc x (target f) by rewrite - sr'; order_tac.
have yt: inc y (target f) by rewrite - sr'; order_tac.
by apply /h1; try Wtac; rewrite (inverse_V bf xt) (inverse_V bf yt).
move=> [inf inif]; red; split => // x y xsf ysf.
move: inf inif=> [_ _ _ h1] [_ _ _ h2].
split; first by move=> hy; apply: h1.
move=> hyp.
rewrite - (inverse_V2 bf xsf) - (inverse_V2 bf ysf).
by apply: h2.
Qed.

Lemma order_isomorphism_opposite g r r':
order_isomorphism g r r' ->
order_isomorphism g (opp_order r) (opp_order r').
Proof.
rewrite /order_isomorphism; move=> [pa pb [pc pd pe] pf].
move: (opp_osr pa) (opp_osr pb) => [qa qb] [qc qd].
split => //; first by split => //; ue.
move => x y xsg ysg.
transitivity (gle r y x) ; first by apply /igraph_pP.
transitivity (gle r' (Vf g y) (Vf g x)); first by apply/(pf _ _ ysg xsg).
symmetry; apply /igraph_pP.
Qed.

We have u v u = u and v u v = v if u and v are decreasing, v (u(x)) and u(v(x)) are both => x

Theorem decreasing_composition u v r r':
decreasing_fun u r r' -> decreasing_fun v r' r ->
(forall x, inc x (substrate r) -> gle r (Vf v (Vf u x)) x) ->
(forall x', inc x' (substrate r') -> gle r' (Vf u (Vf v x')) x') ->
(u \co v \co u = u /\ v \co u \co v = v).
Proof.
move=> [or or' [fu sr sr'] du] [_ _ [fv svr svr'] dv] h h'.
have cvu: v \coP u by split => //; ue.
have fvu: function (v \co u) by fct_tac.
have cuv: u \coP v by split => //; ue.
have fuv: function (u \co v) by fct_tac.
have cuvu: (u \co v) \coP u by split => //; aw; ue.
have cvuv: (v \co u) \coP v by split => //; aw; ue.
split.
apply: function_exten;aw; first by fct_tac.
move=> x xs.
rewrite sr in xs; move:(h _ xs)=> rel1; move: (du _ _ rel1)=> rel2.
have p: inc (Vf u x)(substrate r') by rewrite - sr';Wtac.
move: (h' _ p)=> rel3; aw; try ue.
order_tac.
apply: function_exten; aw; first by fct_tac.
move=> x xs.
rewrite svr in xs; move:(h' _ xs)=> rel1; move: (dv _ _ rel1)=> rel2.
have p: inc (Vf v x) (substrate r) by rewrite - svr';Wtac.
move: (h _ p)=> rel3; aw; try ue.
order_tac.
Qed.

## Maximal and minimal elements

Definition maximal r a :=
inc a (substrate r) /\ forall x, gle r a x -> x = a.
Definition minimal r a :=
inc a (substrate r) /\ forall x, gle r x a -> x = a.

Lemma maximal_opp r: order r -> forall x,
(maximal (opp_order r) x <-> minimal r x).
Proof.
move=> or x; rewrite /maximal /minimal (proj2 (opp_osr or)); split;
move => [xsr h]; split=> // y /igraph_pP;apply: h.
Qed.

Lemma minimal_opp r: order r -> forall x,
(minimal (opp_order r) x <-> maximal r x).
Proof.
move=> or x; rewrite /maximal /minimal (proj2 (opp_osr or)); split;
move => [xsr h]; split=> // y /igraph_pP;apply: h.
Qed.

Example: For inclusion, the empty set is least; if excluded, singletons become minimal

Lemma minimal_inclusion E y (F:= (powerset E) -s1 emptyset):
inc y F -> (minimal (sub_order F) y <-> singletonp y).
Proof.
move=> yF.
rewrite/minimal (proj2 (sub_osr F)).
have Fp: forall x, inc x F <-> (sub x E /\ nonempty x).
rewrite /F=>w; split.
by move/setC1_P => [] /setP_P pa /nonemptyP nw.
by move => [pa /nonemptyP pb]; apply/setC1_P; split=> //; apply/setP_P.
split.
move => [/Fp [yE [z zy]] sp].
have aux: sub (singleton z) y by apply:set1_sub.
have stF: inc (singleton z) F.
apply /Fp; split; [ apply: sub_trans aux yE | apply: set1_ne].
by exists z; symmetry; apply: sp;apply/graph_on_P1.
move=> /singletonP [_ hyp]; split => // x /graph_on_P1 [/Fp [xE [t tx]] _ xy].
apply: extensionality=>//.
by move: (xy _ tx)=> ty z zy; rewrite - (hyp _ _ ty zy).
Qed.

Maximal partial functions for extension order are total functions

Lemma maximal_prolongation E F x:
nonempty F -> inc x (sub_functions E F) ->
(maximal (opp_order (extension_order E F)) x <-> (source x = E)).
Proof.
move: (extension_osr E F) => [eo es].
move=> [t tF] xs; apply: (iff_trans (maximal_opp eo _)).
split.
move: (xs) => /sfun_set_P [fx sx tx][_ h].
apply: extensionality=>// y yE.
ex_middle yns.
have aux: gle (extension_order E F) (extension x y t) x.
rewrite /extension;apply /extension_order_P1; split=> //;last by aw; fprops.
apply /sfun_set_P; split => //; aw.
- apply: extension_f => //.
- by move => z /setU1_P; case; [apply: sx |move=>->].
- rewrite - tx; apply /setU2id_Pr => s /set1_P ->; ue.
by rewrite -(h _ aux); rewrite /extension; aw; fprops.
move=> sx.
red; aw; split; first by ue.
move=> y /extension_orderP [ys _ et].
move: xs ys => /sfun_set_P [fx _ tx] /sfun_set_P [fy sy ty].
move: (extends_Ssource et)=> sy'.
symmetry;apply: function_exten=>//; try ue.
apply: extensionality=>//; ue.
move=> z zs /=; apply: (extends_sV et zs).
Qed.

## Greatest element and least element

Definition greatest r a :=
inc a (substrate r) /\ forall x, inc x (substrate r) -> gle r x a.
Definition least r a :=
inc a (substrate r) /\ forall x, inc x (substrate r) -> gle r a x.

Lemma unique_greatest r: order r -> uniqueness (greatest r).
Proof.
move=> or a b [asr h] [bsr bh].
apply: (order_antisymmetry or (bh _ asr) (h _ bsr)).
Qed.

Lemma unique_least r: order r -> uniqueness (least r).
Proof.
move=> or a b [asr h] [bsr bh].
apply: (order_antisymmetry or (h _ bsr) (bh _ asr)).
Qed.

Definition the_least r := select (least r) (substrate r).
Definition the_greatest r := select (greatest r) (substrate r).

Lemma the_least_pr r:
order r -> (exists u, least r u) ->
least r (the_least r).
Proof.
rewrite /the_least=> or h; apply: (proj1(select_pr _ _)).
by move: h => [z zl];exists z => //; move: zl => [ok _].
by move => x y xsr xlt yset ylt; apply: (unique_least or).
Qed.

Lemma the_greatest_pr r:
order r -> (exists u, greatest r u) ->
greatest r (the_greatest r).
Proof.
rewrite /the_greatest=> or h; apply: (proj1(select_pr _ _)).
by move: h => [z zl]; exists z => //; move: zl => [ok _].
by move => x y xsr xlt ysr ylt; apply: (unique_greatest or).
Qed.

Lemma the_least_pr2 r x:
order r -> least r x -> the_least r = x.
Proof.
move=> or le.
have exu: (exists u, least r u) by exists x.
exact: (unique_least or (the_least_pr or exu) le).
Qed.

Lemma the_greatest_pr2 r x: order r ->
greatest r x -> the_greatest r = x.
Proof.
move=> or le.
have exu: (exists u, greatest r u) by exists x.
exact: (unique_greatest or (the_greatest_pr or exu) le).
Qed.

Lemma greatest_induced r s x:
order r -> sub s (substrate r) -> inc x s ->
greatest r x ->
the_greatest r = the_greatest (induced_order r s).
Proof.
move=> or ssr xs grx.
move: (iorder_osr or ssr) => [pa pb].
rewrite (the_greatest_pr2 or grx).
symmetry; apply: the_greatest_pr2 => //.
red; rewrite pb; split => //.
by move => y yxs; apply/iorder_gleP=> //;apply (proj2 grx); apply: ssr.
Qed.

Lemma least_induced r s x:
order r -> sub s (substrate r) -> inc x s ->
least r x ->
the_least r = the_least (induced_order r s).
Proof.
move=> or ssr xs grx.
move: (iorder_osr or ssr) => [pa pb].
rewrite (the_least_pr2 or grx).
symmetry; apply: the_least_pr2 => //.
red; rewrite pb; split => //.
by move => y yxs; apply/iorder_gleP => //;apply (proj2 grx); apply: ssr.
Qed.

Lemma least_and_greatest r x: order r ->
least r x -> greatest r x ->
singletonp (substrate r).
Proof.
move => or [xs lex][_ gex]; exists x.
apply: (set1_pr xs) => z zs; move: (lex _ zs)(gex _ zs)=> xy yx.
order_tac.
Qed.

Lemma greatest_opposite a r:
order r -> greatest r a -> least (opp_order r) a.
Proof.
by move=> /opp_osr [_ pb] [asr hy]; split; rewrite pb // => x /hy /igraph_pP.
Qed.

Lemma least_opposite a r:
order r -> least r a -> greatest (opp_order r) a.
Proof.
by move=> /opp_osr [_ pb] [asr hy]; split; rewrite pb // => x /hy /igraph_pP.
Qed.

Lemma the_least_opposite r: order r ->
(exists a, greatest r a) ->
the_least (opp_order r) = the_greatest r.
Proof.
move=> or /(the_greatest_pr or) /(greatest_opposite or) hy.
apply: the_least_pr2 => //; apply: (proj1 (opp_osr or)).
Qed.

Lemma greatest_maximal a r:
order r -> greatest r a -> maximal r a.
Proof.
move=> or [asr h]; split=>// x ax;move: (h _ (arg2_sr ax)) => xa; order_tac.
Qed.

Lemma least_minimal a r:
order r -> least r a -> minimal r a.
Proof.
move=> or [asr h]; split=>// x ax;move: (h _ (arg1_sr ax)) => xa; order_tac.
Qed.

Lemma greatest_unique_maximal a b r:
greatest r a -> maximal r b -> a = b.
Proof. by move=> [ar ha][br hb]; apply: hb; apply: ha. Qed.

Lemma least_unique_minimal a b r:
least r a -> minimal r b -> a = b.
Proof.
by move=> [ar ha][br hb]; apply: hb; apply: ha.
Qed.

Examples: subinclusion

Lemma least_is_setI s a:
least (sub_order s) a -> a = intersection s.
Proof.
rewrite /least;move: (sub_osr s) => [_ ->] [asr h].
set_extens x => xs; last by apply: setI_hi xs asr.
apply: setI_i =>//; first by exists a.
by move => y ys; move: (h _ ys) => /graph_on_P1 [_ _ ]; apply.
Qed.

Lemma greatest_is_setU s a:
greatest (sub_order s) a -> a = union s.
Proof.
rewrite /greatest; move :(sub_osr s) => [_ ->] [asr h].
set_extens x => xs;first by union_tac.
by move: (setU_hi xs)=> [y xy ys];move: (h _ ys) => /graph_on_P1 [_ _]; apply.
Qed.

Lemma setI_is_least s:
inc (intersection s) s ->
least (sub_order s) (intersection s) .
Proof.
move=> iis;red; rewrite (proj2 (sub_osr s)); split => //.
by move => x xs;apply/graph_on_P1;split => //; apply: setI_s1.
Qed.

Lemma setU_is_greatest s:
inc (union s) s -> greatest (sub_order s) (union s).
Proof.
move=> iis;red; rewrite (proj2 (sub_osr s)); split => //.
by move=> x xs;apply/graph_on_P1;split; aw; apply: setU_s1.
Qed.

example: inclusion on the powerset

Lemma emptyset_is_least E:
least (subp_order E) emptyset.
Proof.
move:(setP_0i E) => eP.
have h: intersection (powerset E) = emptyset.
by apply /set0_P => t te; move: (setI_hi te eP) => /in_set0.
by rewrite -h;apply: setI_is_least; rewrite h.
Qed.

Lemma wholeset_is_greatest E:
greatest (subp_order E) E.
Proof.
have aux: inc E (powerset E) by apply: setP_Ti.
have h: union (powerset E) = E.
apply:extensionality;last by apply:(setU_s1 aux).
by apply:setU_s2 => y /setP_P.
by rewrite -{2} h; apply:setU_is_greatest; rewrite h.
Qed.

The least function for extension is the empty function; there is generally no greatest

Lemma least_prolongation E F:
least (opp_order (extension_order E F))
(empty_function_tg F).
Proof.
move:(extension_osr E F) => [or sr]; red.
move: (opp_osr or) => [or' ->]; rewrite sr.
have p1:inc (empty_function_tg F) (sub_functions E F).
move: (empty_function_tg_function F) => [pa pb pc].
apply/sfun_set_P;split => //; rewrite pb; fprops.
split=>// x xs; apply/igraph_pP /extension_order_P1; split => //.
rewrite empty_function_graph; fprops.
Qed.

Lemma greatest_prolongation E F x:
greatest (opp_order (extension_order E F)) x ->
nonempty E -> small_set F.
Proof.
move=> ge [t tE].
case: (emptyset_dichot F); first by move=> -> u v uF vF; case: (in_set0 vF).
move:(extension_osr E F) => [oe sr].
move: (opp_osr oe) => []; set (r:= opp_order (extension_order E F)).
move => or sr' neF.
have alc: forall u (Ha:inc u F), x = constant_function E Ha.
move=> u Ha.
set (f:=constant_function E Ha).
have sF: source f = E by rewrite /f/constant_function; aw.
have fsf:inc f (sub_functions E F).
apply /sfun_set_P;split; [by apply: constant_f | ue |].
by rewrite /f/constant_function; aw.
move: sF;rewrite - (maximal_prolongation neF fsf) => sF.
apply :(greatest_unique_maximal ge sF).
move=> u v uF vF.
move: (alc _ vF); rewrite (alc _ uF) => eq.
move: (f_equal (Vf ^~ t) eq); do 2 rewrite constant_V //.
Qed.

If X is a set whose elements are reflexive in E and if the diagonal of E is in X, then it is the least element of X ordered by inclusion, thanks to the next lemma.

Lemma least_equivalence r:
reflexivep r -> sub (diagonal (substrate r)) r.
Proof.
by move=> rr t /diagonal_i_P [pt Ps PQ]; rewrite -pt -PQ; apply: rr.
Qed.

If f:E->F is a bijection, r an ordering on E, there is a unique ordering on F that makes f an isomorphism

Lemma order_transportation f r (r':= image_by_fun (ext_to_prod f f) r) :
bijection f -> order r -> substrate r = source f ->
order_isomorphism f r r'.
Proof.
move=> bf or sr.
have ff: function f by fct_tac.
have fe: function (ext_to_prod f f) by apply: ext_to_prod_f.
have gr: sgraph r by fprops.
have aux: sub r (source (ext_to_prod f f)).
by rewrite /ext_to_prod; aw; rewrite - sr; apply:sub_graph_coarse_substrate.
set (E:= source f).
have zr': (forall z,inc z r' <-> (exists x y, [/\ inc x E, inc y E,
inc (J x y) r & z = J (Vf f x) (Vf f y)])).
move => z; rewrite /r'; split.
move /(Vf_image_P fe aux) => [x xr].
have xJ: J (P x) (Q x) = x by aw; apply: gr.
have pxs: inc (P x) (source f) by rewrite - sr; substr_tac.
have pys: inc (Q x) (source f) by rewrite - sr; substr_tac.
rewrite -xJ (ext_to_prod_V ff ff pxs pys) => ->.
exists (P x), (Q x); split => //; ue.
move=> [x [y [xE yE Jr zJ]]]; apply /(Vf_image_P fe aux); ex_tac.
have xs: inc x (source f) by rewrite - sr; substr_tac.
have ys: inc y (source f) by rewrite - sr; substr_tac.
by rewrite (ext_to_prod_V ff ff xs ys).
have gr': sgraph r' by move=> z; rewrite zr'; move=> [x [y [_ _ _ ->]]]; fprops.
have sr': substrate r' = target f.
set_extens t.
+ case /(substrate_P gr') => [] [y] /zr'[u [v [uE vE Jr zJ]]].
by rewrite (pr1_def zJ); fprops.
by rewrite (pr2_def zJ); fprops.
+ move: bf=> [_ sj] tr; move: ((proj2 sj) _ tr) => [x xsf Wt].
apply: substr_i; rewrite zr'; exists x; exists x.
split=> //; [ order_tac; ue | ue].
suff or': order r'.
red;split => // x y xsr ysr; split.
move =>h;apply /zr'; exists x; exists y;split => //.
move/zr' => [x' [y' [xE' yE' pr sj]]].
move: (pr1_def sj) (pr2_def sj) => w1 w2.
by move: bf => [ [_ h] _]; rewrite (h _ _ xsr xE' w1)(h _ _ ysr yE' w2).
split; first by exact.
- move => y;rewrite sr' => yr; apply/zr'.
move: bf=> [_ sj]; move: ((proj2 sj) _ yr) => [x xsf Wt].
exists x; exists x; rewrite Wt; split => //; order_tac; ue.
- move=>x y z /zr' [a [b [aE bE J1r Jab]]] /zr' [c [d [cE dE J2r Jcd]]].
apply/zr'; exists a; exists d.
have bc: (b = c).
move: bf=> [[_ ij] _ ]; apply: ij =>//.
by rewrite - (pr2_def Jab) - (pr1_def Jcd).
rewrite bc in J1r.
by rewrite - (pr1_def Jab)- (pr2_def Jcd); split => //; order_tac.
- move=> x y /zr' [a [b [aE bE J1r Jab]]] /zr' [c [d [cE dE J2r Jcd]]].
have Wbc: Vf f b = Vf f c by rewrite - (pr2_def Jab) - (pr1_def Jcd).
have Wad: Vf f a = Vf f d by rewrite - (pr1_def Jab) - (pr2_def Jcd).
move: bf=> [[_ ij] _ ].
move:(ij _ _ bE cE Wbc) (ij _ _ aE dE Wad) => eq1 eq2.
have cd: c = d by rewrite eq1 eq2 in J1r; order_tac.
by rewrite (pr1_def Jab) (pr1_def Jcd) eq2 cd.
Qed.

Any ordered set can be extended by adjoining a greatest element

Definition order_with_greatest r a :=
r \cup (((substrate r) +s1 a) *s1 a).

Lemma order_with_greatest_pr r a (r':=order_with_greatest r a):
order r -> ~ (inc a (substrate r)) ->
[/\ order_on r' ((substrate r) +s1 a),
r = induced_order r' (substrate r) & greatest r' a].
Proof.
rewrite /r' /order_with_greatest => or nas {r'}.
set (E:=substrate r).
set r':= union2 r _.
have jaa: inc (J a a) ((E +s1 a) *s1 a) by apply: indexed_pi; fprops.
have src:sub r (coarse E)
by rewrite /E; apply: sub_graph_coarse_substrate; fprops.
have gr': sgraph r' by rewrite /r'/indexed; apply: setU2_graph; fprops.
have sr': substrate r'= E +s1 a.
set_extens x.
rewrite /E =>t; apply/setU1_P.
case /(substrate_P gr'):t => [][y] /setU2_P [];
try (left; rewrite /E;substr_tac); move/setXp_P => [];
[by move/setU1_P | by move => _ /set1_P => h;right].
case /setU1_P => hh; apply: substr_i; first by apply:setU2_1; order_tac.
by rewrite hh; apply:setU2_2.
have rr: reflexivep r'.
move => y;rewrite sr';case /setU1_P.
by move=> hyp;apply:setU2_1; order_tac.
move=> ->;apply:setU2_2; fprops.
have tr:transitivep r'.
move=> x y z;case /setU2_P=> h; case /setU2_P=> h'.
+ apply:setU2_1; order_tac.
+ apply:setU2_2; apply/setXp_P; move/setXp_P: h' => [pa pb];split => //.
apply:setU2_1; rewrite /E; substr_tac.
+ move/setXp_P: h => [pa pb]; case: nas; move/set1_P: pb => <-; substr_tac.
+ move/setXp_P: h' => [_] /set1_P ->; move/setXp_P: h => [pb] _.
by apply:setU2_2; apply: indexed_pi.
have ar:antisymmetricp r'.
move=> x y;case /setU2_P=> h; case /setU2_P=> h'.
+ order_tac.
+ case: nas; move/setXp_P: h' => [_] /set1_P <-; substr_tac.
+ case: nas; move/setXp_P: h => [_] /set1_P <-; substr_tac.
+ by move/setXp_P: h => [_] /set1_P ->; move/setXp_P: h' => [_] /set1_P ->.
have or': order r' by [].
split => //.
rewrite /r' /induced_order; set_extens x => xr.
by apply: setI2_i; [ apply/setU2_P; left| apply: src].
case/setI2_P: xr => /setU2_P [] //.
by move /setX_P => [_ _] /set1_P qa /setX_P [_ _]; rewrite qa.
red; rewrite sr'; split; fprops.
by move=> x xe; apply /setU2_P; right; apply: indexed_pi.
Qed.

order r -> substrate r = E -> ~ (inc a E) ->
exists !r', [/\ order_on r' (E +s1 a),
r = induced_order r' E & greatest r' a].
Proof.
move=> or sr naE.
set (E':=E +s1 a).
set (r':=r \cup (E' \times (singleton a))).
apply /unique_existence; split.
exists (order_with_greatest r a).
rewrite - sr in naE; move: (order_with_greatest_pr or naE).
by rewrite sr.
pose p x := [/\ order_on x E', r = x \cap (coarse E) & greatest x a].
suff : forall x y, p x -> p y -> sub x y.
move=> hyp x y px py.
apply: extensionality; [ apply: hyp px py | apply: hyp py px].
move=> x y [[ox sx] ix gx] [[oy sy] iy gy] z zx.
have pz: pairp z by apply: (_ : sgraph x); fprops.
have PzE: inc (P z) E' by rewrite - sx; substr_tac.
have QzE: inc (Q z) E' by rewrite - sx; substr_tac.
case/setU1_P: PzE=> Pz.
case /setU1_P: QzE=> Qz.
have: (inc z r) by rewrite ix;apply: setI2_i=> //; apply /setX_P.
by rewrite iy; move /setI2_P => [].
move: gy=>[ay ga];rewrite -pz Qz; apply: ga; rewrite sy /E'; fprops.
case /setU1_P: QzE => Qz.
have rel2 : gle x (Q z) (P z).
move: gx=>[ax ga]; rewrite Pz; apply: ga; rewrite sx /E'; fprops.
have rel1 : gle x (P z) (Q z) by red; red; rewrite pz.
have PQ: P z = Q z by order_tac.
by case: naE; rewrite -Pz PQ.
rewrite -pz Qz; move: gy=>[ax]; apply; ue.
Qed.

A set A is cofinal (resp. coinitial) if every element of E is bounded above (resp. below) by an element of A

Definition cofinal r a :=
sub a (substrate r) /\
(forall x, inc x (substrate r) -> exists2 y, inc y a & gle r x y).

Definition coinitial r a :=
sub a (substrate r) /\
(forall x, inc x (substrate r) -> exists2 y, inc y a & gle r y x).

Lemma exists_greatest_cofinalP r:
(exists x, greatest r x) <->
(exists2 a, cofinal r a & singletonp a).
Proof.
split.
move=> [a [asr h]]; exists (singleton a).
split; first by move=> t /set1_P ->.
move=> x xr; exists a;fprops.
by exists a.
move=> [a [asr h] [b bp]];exists b;split.
apply: asr; rewrite bp; fprops.
by move=> x xsr; move:(h _ xsr)=> [y]; rewrite bp; move /set1_P => ->.
Qed.

Lemma exists_least_coinitialP r:
(exists x, least r x) <->
(exists2 a, coinitial r a & singletonp a).
Proof.
split.
move=> [a [asr h]]; exists (singleton a).
split; first by move=> t /set1_P ->.
move=> x xr; exists a; fprops.
by exists a.
move=> [a [asr h] [b bp]];exists b;split.
apply: asr; rewrite bp; fprops.
by move=> x xsr; move:(h _ xsr)=> [y]; rewrite bp; move /set1_P => ->.
Qed.

## Upper and lower bounds

Definition upper_bound r X x :=
inc x (substrate r) /\ forall y, inc y X -> gle r y x.
Definition lower_bound r X x :=
inc x (substrate r) /\ forall y, inc y X -> gle r x y.

Lemma opposite_upper_boundP r: order r -> forall X x,
(upper_bound r X x <-> lower_bound (opp_order r) X x).
Proof.
rewrite /upper_bound/lower_bound=> or X; rewrite (proj2 (opp_osr or)).
by split; move=> [xsr h]; split=>//; move=> y yR; move:(h _ yR); move/igraph_pP.
Qed.

Lemma opposite_lower_boundP r: order r -> forall X x,
(lower_bound r X x <-> upper_bound (opp_order r) X x).
Proof.
rewrite /upper_bound/lower_bound=> or X x; rewrite (proj2 (opp_osr or)).
by split; move=> [xsr h]; split=>//; move=> y yR; move:(h _ yR); move/igraph_pP.
Qed.

Lemma smaller_lower_bound x y X r: preorder r ->
lower_bound r X x -> gle r y x -> lower_bound r X y.
Proof.
rewrite /lower_bound=> [] [rr _ tr] [xH h] yx.
split; first by red in yx;substr_tac.
move=> z zX; apply: tr yx (h _ zX).
Qed.

Lemma greater_upper_bound x y X r: preorder r ->
upper_bound r X x -> gle r x y -> upper_bound r X y.
Proof.
rewrite /lower_bound=> [] [rr _ tr] [xH h] yx.
split; first by red in yx;substr_tac.
move=> z zX; apply: tr (h _ zX) yx.
Qed.

Lemma sub_lower_bound x X Y r:
lower_bound r X x -> sub Y X-> lower_bound r Y x.
Proof.
rewrite /lower_bound=> [] [xR lo] YX .
split=>//; move=> y yY; apply: lo (YX _ yY).
Qed.

Lemma sub_upper_bound x X Y r:
upper_bound r X x -> sub Y X -> upper_bound r Y x.
Proof.
rewrite /lower_bound=> [] [xR lo] YX .
split=>//; move=> y yY; apply: lo (YX _ yY).
Qed.

Lemma least_elementP X r: order r -> sub X (substrate r) ->
((exists a, least (induced_order r X) a) <->
(exists2 x, lower_bound r X x & inc x X)).
Proof.
rewrite /lower_bound/least=> or Xr.
rewrite (proj2 (iorder_osr or Xr)); split.
move=> [a [aX h]]; exists a => //;split; first by apply:Xr.
move=> y yX; move: (h _ yX); apply:iorder_gle1.
move=> [x [xsr hyp] xX]; ex_tac.
by move=> y yX; apply/iorder_gleP => //; apply: hyp.
Qed.

Lemma greatest_elementP X r: order r -> sub X (substrate r) ->
((exists a, greatest (induced_order r X) a) <->
(exists2 x, upper_bound r X x & inc x X)).
Proof.
rewrite /upper_bound/greatest=> or Xr.
rewrite (proj2 (iorder_osr or Xr)); split.
move=> [a []]; aw=> aX h; exists a => //;split; first by apply:Xr.
move=> y yX; move: (h _ yX); apply:iorder_gle1.
move=> [x [xsr hyp] xX]; ex_tac.
by move=> y yX; apply/iorder_gleP => //; apply: hyp.
Qed.

A set can be bounded above, below, or both

Definition bounded_above r X := exists x, upper_bound r X x.
Definition bounded_below r X := exists x, lower_bound r X x.
Definition bounded_both r X := bounded_above r X /\ bounded_below r X.

Lemma bounded_above_sub X Y r:
sub Y X -> bounded_above r X -> bounded_above r Y.
Proof. move=> YX [x ux]; exists x; apply: (sub_upper_bound ux YX). Qed.

Lemma bounded_below_sub X Y r:
sub Y X -> bounded_below r X -> bounded_below r Y.
Proof. move=> YX [x ux]; exists x; apply: (sub_lower_bound ux YX). Qed.

Lemma bounded_both_sub X Y r:
sub Y X -> bounded_both r X -> bounded_both r Y.
Proof.
rewrite /bounded_both=> YX [p1 p2].
split; [ apply: (bounded_above_sub YX p1) | apply: (bounded_below_sub YX p2)].
Qed.

Lemma singleton_bounded x r:
singletonp x -> order r -> sub x (substrate r) -> bounded_both r x.
Proof.
move=> [y yp] or xsr.
have ysr: inc y (substrate r) by apply: xsr;rewrite yp; fprops.
have yy: gle r y y by order_tac.
by split; exists y; split=>//; rewrite yp; move=> z /set1_P=> ->.
Qed.

## Least upper bound and greatest lower bound

Definition greatest_lower_bound r X x :=
greatest (induced_order r (Zo (substrate r) (lower_bound r X))) x.
Definition least_upper_bound r X x :=
least (induced_order r (Zo (substrate r) (upper_bound r X))) x.

Lemma glbP r X:
order r -> sub X (substrate r) -> forall x,
(greatest_lower_bound r X x <-> (lower_bound r X x
/\ forall z, lower_bound r X z -> gle r z x)).
Proof.
rewrite /greatest_lower_bound/greatest=> or Xr x.
set T:= Zo _ _.
have sT: sub T (substrate r) by apply: Zo_S.
rewrite (proj2 (iorder_osr or sT)).
split.
move=> [xT hyp]; move: (xT) => /Zo_P [xsr lb]; split=>//.
move=> z lbz.
have zT: inc z T by apply: Zo_i=>//; move: lbz=> [].
move: (hyp _ zT); apply: iorder_gle1.
move=> [lbx hyp].
have xT: inc x T by rewrite /T Zo_P; split=>//; move: lbx=> [].
split=>//; move=> y yT; apply /iorder_gleP=> //.
move: yT => /Zo_P [_]; apply: hyp.
Qed.

Lemma lubP r X:
order r -> sub X (substrate r) -> forall x,
(least_upper_bound r X x <-> (upper_bound r X x
/\ forall z, upper_bound r X z -> gle r x z)).
Proof.
rewrite /least_upper_bound/least=>or Xr x.
set T:= Zo _ _.
have sT: sub T (substrate r) by apply: Zo_S.
rewrite (proj2 (iorder_osr or sT)).
split.
move=> [xT hyp]; move: (xT) => /Zo_P [xsr lb]; split=>//.
move=> z lbz.
have zT: inc z T by apply: Zo_i=>//; move: lbz=> [].
by move: (hyp _ zT); apply: iorder_gle1.
move=> [lbx hyp].
have xT: inc x T by apply: Zo_i=>//; move: lbx=> [].
split=>//; move=> y yT; apply /iorder_gleP=> //.
move: yT => /Zo_P [_]; apply: hyp.
Qed.

Lemma supremum_unique X r: order r -> uniqueness (least_upper_bound r X).
Proof.
rewrite /least_upper_bound => or.
exact:(unique_least (proj1 (iorder_osr or (Zo_S (p:=upper_bound r X))))).
Qed.

Lemma infimum_unique X r: order r -> uniqueness (greatest_lower_bound r X).
Proof.
rewrite /greatest_lower_bound => or.
exact: (unique_greatest (proj1 (iorder_osr or (Zo_S (p:=lower_bound r X))))).
Qed.

Definition of the supremum or infimum of a set or a pair

Definition infimum r X :=
the_greatest (induced_order r (Zo (substrate r) (lower_bound r X))).
Definition supremum r X :=
the_least (induced_order r (Zo (substrate r) (upper_bound r X))).
Definition sup r x y := supremum r (doubleton x y).
Definition inf r x y := infimum r (doubleton x y).
Definition has_supremum r X := (exists x, least_upper_bound r X x).
Definition has_infimum r X := (exists x, greatest_lower_bound r X x).

Lemma supremum_pr1 X r:
order r -> has_supremum r X ->
least_upper_bound r X (supremum r X).
Proof.
move => or [z h].
apply: the_least_pr => //; last by exists z.
apply: (proj1 (iorder_osr or (Zo_S(p:=upper_bound r X)))).
Qed.

Lemma infimum_pr1 X r:
order r -> has_infimum r X ->
greatest_lower_bound r X (infimum r X).
Proof.
move => or [z h].
apply: the_greatest_pr => //; last by exists z.
apply: (proj1 (iorder_osr or (Zo_S(p:=lower_bound r X)))).
Qed.

Hint Resolve supremum_pr1 infimum_pr1: fprops.

Lemma supremum_pr2 r X a: order r ->
least_upper_bound r X a -> a = supremum r X.
Proof.
move=> or le.
have hs: has_supremum r X by exists a.
apply: (supremum_unique or le (supremum_pr1 or hs)).
Qed.

Lemma infimum_pr2 r X a: order r ->
greatest_lower_bound r X a -> a = infimum r X.
Proof.
move=> or le.
have hs: has_infimum r X by exists a.
apply: (infimum_unique or le (infimum_pr1 or hs)).
Qed.

Lemma inc_supremum_substrate X r:
order r -> sub X (substrate r) -> has_supremum r X ->
inc (supremum r X) (substrate r).
Proof.
move=> or Xsr hs.
by move: (supremum_pr1 or hs)=> /(lubP or Xsr) [[aa _] _].
Qed.

Lemma inc_infimum_substrate X r:
order r -> sub X (substrate r) -> has_infimum r X ->
inc (infimum r X) (substrate r).
Proof.
move=> or Xsr hs.
by move: (infimum_pr1 or hs)=> /(glbP or Xsr) [[aa _] _].
Qed.

Lemma supremum_pr X r:
order r -> sub X (substrate r) -> has_supremum r X ->
(upper_bound r X (supremum r X) /\
forall z, upper_bound r X z -> gle r (supremum r X) z).
Proof. by move=> or Xsr /(supremum_pr1 or) /(lubP or Xsr). Qed.

Lemma infimum_pr X r:
order r -> sub X (substrate r) -> has_infimum r X ->
(lower_bound r X (infimum r X) /\
forall z, lower_bound r X z -> gle r z (infimum r X)).
Proof. by move=> or Xsr /(infimum_pr1 or) /(glbP or Xsr). Qed.

Properties of sup and inf of pairs

Lemma sup_pr a b r:
order r -> inc a (substrate r) -> inc b (substrate r)
-> has_supremum r (doubleton a b) ->
[/\ gle r a (sup r a b), gle r b (sup r a b) &
forall z, gle r a z -> gle r b z -> gle r (sup r a b) z].
Proof.
move=> or ast bsr hs.
have sd: sub (doubleton a b) (substrate r) by apply: sub_set2.
move: (supremum_pr or sd hs) => [[sr h1] h2]; split; try apply: h1; fprops.
move=> z az bz; apply: h2.
split; [by order_tac | by move=>y; case /set2_P => ->].
Qed.

Lemma inf_pr a b r:
order r -> inc a (substrate r) -> inc b (substrate r)
-> has_infimum r (doubleton a b) ->
[/\ gle r (inf r a b) a, gle r (inf r a b) b &
forall z, gle r z a -> gle r z b -> gle r z (inf r a b)].
Proof.
move=> or ast bsr hs.
have sd: sub (doubleton a b) (substrate r) by apply: sub_set2.
move: (infimum_pr or sd hs) => [[sr h1] h2]; split; try apply: h1; fprops.
move=> z az bz; apply: h2.
split; [by order_tac | by move=>y; case /set2_P => ->].
Qed.

Lemma lub_set2 r x y z:
order r -> gle r x z -> gle r y z ->
(forall t, gle r x t -> gle r y t -> gle r z t) ->
least_upper_bound r (doubleton x y) z.
Proof.
move=> or xz yz h.
move:(arg1_sr xz)(arg1_sr yz) => xsr ysr.
apply/(lubP or); first by move=>t /set2_P;case => ->.
split; first by split; [order_tac | by move=>t /set2_P;case => ->].
move=> t [_ tb]; apply: h; apply: tb; fprops.
Qed.

Lemma glb_set2 r x y z:
order r -> gle r z x -> gle r z y ->
(forall t, gle r t x -> gle r t y -> gle r t z) ->
greatest_lower_bound r (doubleton x y) z.
Proof.
move=> or xz yz h.
move:(arg2_sr xz) (arg2_sr yz) => xsr ysr.
apply/(glbP or); first by move=>t /set2_P;case => ->.
split;first by split; [order_tac | by move=>t /set2_P;case => ->].
move=> t [_ tb]; apply: h; apply: tb; fprops.
Qed.

Link between supremum and greatest element

Lemma greatest_is_sup r X a:
order r -> sub X (substrate r) ->
greatest (induced_order r X) a -> least_upper_bound r X a.
Proof.
move=> or Xsr []; rewrite (proj2 (iorder_osr or Xsr)) => aX h.
apply/(lubP or Xsr); split.
split; [by apply: Xsr | move=> y yX; move: (h _ yX); apply:iorder_gle1 ].
by move=> z [zs h2]; apply: (h2 _ aX).
Qed.

Lemma least_is_inf r X a:
order r -> sub X (substrate r) ->
least (induced_order r X) a -> greatest_lower_bound r X a.
Proof.
move=> or Xsr []; rewrite (proj2 (iorder_osr or Xsr)) => aX h.
apply/(glbP or Xsr); split.
split; [by apply: Xsr | by move=> y yX; move: (h _ yX); apply:iorder_gle1].
by move=> z [zs h2]; apply: (h2 _ aX).
Qed.

Lemma inf_sup_oppP r X:
order r -> sub X (substrate r) -> forall a,
(greatest_lower_bound r X a <-> least_upper_bound (opp_order r) X a).
Proof.
move=> or Xsr a.
move: (opp_osr or) => [oor osr].
have Xsor: sub X (substrate (opp_order r)) by ue.
apply:(iff_trans (glbP or Xsr a)); symmetry; apply:(iff_trans(lubP oor Xsor a)).
split; move => [pa pb]; split;
try (apply /(opposite_lower_boundP or) => //);
by move => z /(opposite_lower_boundP or) => h; apply/igraph_pP; apply: pb.
Qed.

Lemma sup_inf_oppP r X:
order r -> sub X (substrate r) -> forall a,
(least_upper_bound r X a <-> greatest_lower_bound (opp_order r) X a).
Proof.
move=> or Xsr a; symmetry.
move: (opp_osr or) => [oor osr].
have Xsor: sub X (substrate (opp_order r)) by ue.
move: (inf_sup_oppP oor Xsor a).
have -> //: (opp_order (opp_order r) = r) by apply igraph_involutive; fprops.
Qed.

Supremum and infimum of the empty set

Lemma set_of_lower_bounds_set0 r:
Zo (substrate r) (lower_bound r emptyset) = substrate r.
Proof.
apply: extensionality; first by apply: Zo_S.
move=> x xsr; apply /Zo_P; split=>//; split=>// y;case; case.
Qed.

Lemma set_of_upper_bounds_set0 r:
Zo (substrate r) (upper_bound r emptyset) = substrate r.
Proof.
apply: extensionality; first by apply: Zo_S.
move=> x xsr; apply /Zo_P; split=>//; split=>// y;case; case.
Qed.

Lemma lub_set0 r: order r -> forall x,
(least_upper_bound r emptyset x = least r x).
Proof.
move=> or; rewrite /least_upper_bound set_of_upper_bounds_set0.
by rewrite iorder_substrate.
Qed.

Lemma glb_set0 r: order r -> forall x,
greatest_lower_bound r emptyset x = greatest r x.
Proof.
move=> or; rewrite /greatest_lower_bound set_of_lower_bounds_set0.
by rewrite iorder_substrate.
Qed.

Supremum and infimum for inclusion order

Lemma setI_inf s E: sub s (powerset E) ->
greatest_lower_bound (subp_order E) s
(Yo (nonempty s) (intersection s) E).
Proof.
move=> sp.
move:(subp_osr E) => [oi si1].
have nee: ~ nonempty emptyset by move/nonemptyP.
case: (emptyset_dichot s)=> h.
rewrite h Y_false // glb_set0 //.
by apply: wholeset_is_greatest.
Ytac0.
have si: sub (intersection s) E.
move: h=> [y ys]; apply: (@sub_trans y).
by apply: setI_s1.
by move: (sp _ ys) => /setP_P.
have ss: sub s (substrate (subp_order E)) by rewrite si1.
apply/(glbP oi ss); rewrite /lower_bound si1; split.
split; first by apply/setP_P.
move=> y ys; apply /subp_gleP; split => //.
by apply/setP_P; apply: sp.
by apply: setI_s1.
move=> z []/setP_P => zE hyp.
apply /subp_gleP;split => //; move=> t tz; apply: (setI_i h) => y ys.
by move: (hyp _ ys) => /subp_gleP [_ _]; apply.
Qed.

Lemma setU_sup s E: sub s (powerset E) ->
least_upper_bound (subp_order E) s (union s).
Proof.
move=> sp.
move:(subp_osr E) => [oi si1].
have su:sub (union s) E.
by apply: setU_s2; move=> y ys; move: (sp _ ys) => /setP_P.
have aux: sub s (substrate (subp_order E)) by ue.
apply/(lubP oi aux); rewrite /upper_bound si1; split.
split; first by apply/setP_P.
move => y ys.
have sy: sub y (union s) by apply: setU_s1.
by apply/subp_gleP; split => //; move: (sp _ ys) => /setP_P.
move=> z [zE hyp]; apply/subp_gleP; split => //; first by apply/setP_P.
apply: setU_s2 => y ys; move: (hyp _ ys) => /subp_gleP [_ _]; apply.
Qed.

Lemma setU_sup1 s F E: sub F (powerset E) ->
sub s F -> inc (union s) F ->
least_upper_bound (sub_order F) s (union s).
Proof.
move=> Fp sF uF.
move:(sub_osr F) => [oi si1].
have sss: sub s (substrate (sub_order F)) by ue.
apply/(lubP oi sss); rewrite /upper_bound si1; split.
split => //; move=> y ys.
by apply /sub_gleP; split => //; fprops;apply: setU_s1.
move=> z [zF hyp]; apply /sub_gleP; split => //.
apply: setU_s2=> y ys; move: (hyp _ ys) => /sub_gleP [_ _]; apply.
Qed.

Lemma setI_inf1 s F E (T := (Yo (nonempty s) (intersection s) E)):
sub F (powerset E) ->
sub s F -> inc T F ->
greatest_lower_bound (sub_order F) s T.
Proof.
rewrite /T;move=> Fp sF ssF.
move:(sub_osr F) => [oi si1].
have sss: sub s (substrate (sub_order F)) by ue.
apply/(glbP oi sss); rewrite /lower_bound si1; split.
split =>// y ys; apply /sub_gleP; split; fprops.
have nes: (nonempty s) by exists y.
Ytac0;apply: setI_s1=>//.
move=>z [zF hyp]; apply /sub_gleP; split => //.
case: (emptyset_dichot s) => sp.
by rewrite Y_false;[apply /setP_P /Fp | rewrite sp; move /nonemptyP ].
Ytac0;move=> t tz; apply: setI_i=>//.
by move=> y ys; move: (hyp _ ys) => /sub_gleP [_ _]; apply.
Qed.

Supremum for extension order: is least common extension

Lemma sup_extension_order1 E F T f:
sub T (sub_functions E F) ->
least_upper_bound (opp_order (extension_order E F)) T f ->
forall u v x, inc u T -> inc v T -> inc x (source u) -> inc x (source v) ->
Vf u x = Vf v x.
Proof.
move=> Ts lef.
move:(extension_osr E F)=> [oe sr].
move: (opp_osr oe) => [oo so].
have sTe: sub T (substrate (extension_order E F)) by ue.
have sT:sub T (substrate (opp_order (extension_order E F))) by ue.
move: lef => /(lubP oo sT) [[fs ub] hyp] u v x uT vT xs ys.
by rewrite (extension_order_pr (ub _ uT) xs) (extension_order_pr (ub _ vT) ys).
Qed.

Lemma sup_extension_order2 E F T:
sub T (sub_functions E F) ->
(forall u v x, inc u T -> inc v T -> inc x (source u) -> inc x (source v) ->
Vf u x = Vf v x) ->
exists x, [/\ least_upper_bound (opp_order (extension_order E F)) T x,
(source x = unionb (Lg T source)),
(range (graph x) = unionb (Lg T (fun u => (range (graph u))))) &
(graph