# Theory of Sets EIII-2 Well ordered sets

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

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

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

Module Worder.

## EIII-2-1 Segments of a well-ordered set

Well ordering

Definition worder r :=
order r /\ forall x, sub x (substrate r) -> nonempty x ->
exists y, least (induced_order r x) y.

Definition worder_r (r: relation) :=
order_r r /\ forall x, (forall a, inc a x -> r a a) -> nonempty x ->
exists y, least (graph_on r x) y.

Definition worder_on G E := worder G /\ substrate G = E.

Lemma worder_or r: worder r -> order r.
Proof. move=> [or _]; exact or. Qed.

Hint Resolve worder_or: fprops.

Lemma wordering_pr r x:
worder_r r -> (forall a, inc a x -> r a a) ->
worder_on (graph_on r x) x.
Proof.
move=> [or wo] ar.
have sg: (substrate (graph_on r x) = x) by bw.
have gor: order (graph_on r x) by apply: order_from_rel.
split=>//; split=>//.
rewrite sg; move=> s sx nes.
have rs: (forall a, inc a s -> r a a) by move=> a /sx/ar.
have sgs: substrate (graph_on r s) = s by bw.
move: (wo _ rs nes)=> [a []]; rewrite sgs => ais lea.
have ss:sub s (substrate (graph_on r x)) by rewrite sg.
exists a; split; first by aw; ue.
move=> y;rewrite (iorder_sr gor ss) => ys; aw.
move: (lea _ ys) => /graph_on_P1 [pa pb pc]; apply/iorder_gleP => //.
by apply/graph_on_P1;split => //; apply: sx.
Qed.

The empty set is well-ordered

Lemma set0_or: order emptyset.
Proof. rewrite - setI_0; apply: setIrel_or => t;case; case. Qed.

Lemma set0_wor: worder_on emptyset emptyset.
Proof.
have aux: substrate emptyset = emptyset.
by rewrite /substrate domain_set0 range_set0 setU2_id.
split; [ split; [apply: set0_or | rewrite aux ] | exact: aux].
move=> x xs [y yx]; case: (in_set0 (xs _ yx)).
Qed.

Lemma empty_substrate_zero x: substrate x = emptyset ->
x = emptyset.
Proof.
move => aux; apply /domain_set0_P; apply /set0_P => y h.
by empty_tac1 y; apply /setU2_P; left.
Qed.

Singletons are well-ordered, and isomorphic

Lemma set1_wor x: worder_on (singleton (J x x)) (singleton x).
Proof.
set G := (singleton (J x x)).
have Ei: (G = diagonal (singleton x)).
set_extens t; first by move /set1_P => ->; apply/diagonal_pi_P;fprops.
move/diagonal_i_P => [pa] /set1_P pb pc; apply/set1_P.
by rewrite - pa -pc pb.
move:(diagonal_osr (singleton x)) => [pa pb].
have oE: (order G) by rewrite Ei.
have sE: (substrate G = singleton x) by rewrite Ei pb.
split =>//; split =>//.
move=> y yE [z zy]; exists z; red; aw;split => //.
move=> t ty; apply/iorder_gleP => //.
rewrite sE in yE.
by rewrite (set1_eq (yE _ zy)) (set1_eq (yE _ ty)); apply/set1_P.
Qed.

Lemma set1_order_is x y:
(singleton (J x x)) \Is (singleton (J y y)).
Proof.
move: (set1_wor x) => [[o1 _] s1].
move: (set1_wor y) => [[o2 _] s2].
have ta: lf_axiom (fun _ : Set => y) (singleton x) (singleton y).
by move=> t;fprops.
exists (Lf (fun _ => y) (singleton x) (singleton y)).
red; split => //.
rewrite s1 s2; split; aw => //.
apply lf_bijective => //.
by move=> u v /set1_P -> /set1_P ->.
move=> t /set1_P ->; exists x;fprops.
move=> a b; rewrite lf_source => pa pb; aw.
split; move => _; first by apply/set1_P.
move /set1_P: pa => ->; move /set1_P: pb => ->; by apply/set1_P.
Qed.

Lemma set1_order_is1 r:
order r -> singletonp (substrate r) ->
exists x, r = singleton (J x x).
Proof.
move=> or [u sxsu]; exists u; set_extens v; aw.
move=> vx; move: ((order_sgraph or) _ vx) => p.
rewrite - p in vx |- *.
move: (arg1_sr vx) (arg2_sr vx);rewrite sxsu.
by move /set1_P => -> /set1_P ->; apply/set1_P.
move/set1_P => ->; order_tac;rewrite sxsu; fprops.
Qed.

Lemma set1_order_is2 r r':
order r -> order r' ->
singletonp (substrate r) -> singletonp (substrate r')
-> r \Is r'.
Proof.
move=> ox oy ssx ssy.
move: (set1_order_is1 ox ssx)=> [u ->].
move: (set1_order_is1 oy ssy)=> [v ->].
apply: set1_order_is.
Qed.

Lemma worder_set1 r e: order_on r (singleton e) -> worder r.
Proof.
move=> [or sr].
suff: r = singleton (J e e) by move => ->; exact (proj1(set1_wor e)).
apply: set1_pr; first by order_tac; rewrite sr; fprops.
move=> t tr; rewrite - (order_sgraph or tr).
move: (pr1_sr tr) (pr2_sr tr); rewrite sr.
by move => /set1_P -> /set1_P ->.
Qed.

We sometimes need an ordered set with two elements; It is well-ordered

Definition canonical_doubleton_order :=
(tripleton (J C0 C0) (J C1 C1) (J C0 C1)).

Lemma cdo_gleP x y:
gle canonical_doubleton_order x y <->
[\/ (x = C0 /\ y = C0), (x = C1 /\ y = C1) | (x = C0 /\ y = C1)].
Proof.
split.
case/set3_P; move => h;rewrite(pr1_def h)(pr2_def h); in_TP4.
case; move=> [-> ->]; apply /set3_P; in_TP4.
Qed.

Lemma cdo_wor: worder_on canonical_doubleton_order C2.
Proof.
have cg: sgraph canonical_doubleton_order.
by move => t /set3_P; case => ->; fprops.
have subs: substrate canonical_doubleton_order = C2.
set_extens x.
case/(substrate_P cg) => [] [y] /cdo_gleP.
case;case => ->; fprops.
case;case => _ ->; fprops.
case /C2_P => ->; apply: substr_i; apply /cdo_gleP; in_TP4.
have oc: (order canonical_doubleton_order).
red; split => //.
move => y;rewrite subs; case /C2_P => ->; apply /cdo_gleP; in_TP4.
move=> x y z /cdo_gleP pa /cdo_gleP pb; apply /cdo_gleP.
have aux: z = C0 \/ z = C1 by case: pb;move => [_ ->]; [left |right |right].
case: (equal_or_not y C0); first by move => ->; case :aux => ->; in_TP4.
case: pa; move => [-> pa] //.
move: pa; case: pb; move => [-> ->]; in_TP4.
move=> x y /cdo_gleP pa /cdo_gleP.
by case: pa; move=> [-> ->] //; case; try move => [ aa bb].
split; [split =>// x xt nex | exact].
rewrite /least (proj2 (iorder_osr oc xt)).
case: (inc_or_not C0 x)=> hyp.
ex_tac => y yx; apply iorder_gleP => //; apply /cdo_gleP.
move: (xt _ yx); rewrite subs; case /C2_P => ye; in_TP4.
move: nex=> [y yx]; ex_tac.
have p: forall t, inc t x -> t = C1.
move=> t tx; move: (xt _ tx); rewrite subs; case/C2_P => //.
by move => ta;rewrite ta in tx; case: hyp.
move => t tx; apply iorder_gleP => //; apply /cdo_gleP.
by rewrite (p _ yx)(p _ tx); constructor 2.
Qed.

A well ordering is total; bounded sets have a supremum

Lemma worder_total r: worder r -> total_order r.
Proof.
move=> [or wo]; split=>//.
move=> x y xs ys.
set (u:=doubleton x y).
have xu: (inc x u) by rewrite /u; fprops.
have yu: (inc y u) by rewrite /u; fprops.
have ur: sub u (substrate r) by rewrite /u; apply: sub_set2.
have si: substrate (induced_order r u) = u by aw.
have neu: nonempty u by ex_tac.
move: (wo _ ur neu)=> [z []]; rewrite si => zu zle.
have aux: forall t, inc t u -> gle r z t.
by move => t tu; move:(iorder_gle1 (zle _ tu)).
move: (aux _ xu)(aux _ yu) => p1 p2.
by case /set2_P: zu => <-; [left | right].
Qed.

Lemma worderr_total r x y: worder_r r -> r x x -> r y y ->
(r x y \/ r y x).
Proof.
move => [p1 p2] rxx ryy.
set (u:=doubleton x y).
have xu: (inc x u) by rewrite /u; fprops.
have yu: (inc y u) by rewrite /u; fprops.
have p3: (forall a, inc a u -> r a a).
by move => a /set2_P; case => ->.
have p4: nonempty u by ex_tac.
have p5:(substrate (graph_on r u)) = u by apply: graph_on_sr.
move: (p2 _ p3 p4)=> [z []]; rewrite p5 => zu zle.
move: (zle _ xu) => /graph_on_P1 [_ _ zx].
move: (zle _ yu) => /graph_on_P1 [_ _ zy].
by case /set2_P: zu => <-; [left | right].
Qed.

Lemma worder_hassup r A: worder r -> sub A (substrate r) ->
bounded_above r A -> has_supremum r A.
Proof.
move=> [or wo] As [t tA].
red; rewrite /least_upper_bound.
set X:= (Zo _ _).
have Xs: sub X (substrate r) by apply: Zo_S.
have nX: (nonempty X).
by exists t; apply: Zo_i =>//; move: tA=> [tA _].
by move: (wo _ Xs nX)=> [x leX]; exists x.
Qed.

Lemma induced_wor r A: worder r -> sub A (substrate r) ->
worder (induced_order r A).
Proof.
move=> [or wo] As; move: (iorder_osr or As) => [pa pb].
split; [exact | rewrite pb => x sx nex].
rewrite (iorder_trans _ sx).
by apply: wo=>//; apply: sub_trans As.
Qed.

Lemma worder_least r: worder r -> nonempty (substrate r) ->
exists y, least r y.
Proof.
move=> [or wo] ne.
move: (wo _ (@sub_refl (substrate r)) ne)=> [x lex].
rewrite iorder_substrate // in lex.
by exists x.
Qed.

A set remains well-ordered after adjoining a greatest element

Lemma worder_adjoin_greatest r a: worder r-> ~ (inc a (substrate r))
-> worder (order_with_greatest r a).
Proof.
move=> [or wo] nas.
move: (order_with_greatest_pr or nas) => [[on sn] rd gna].
split=>// x xs nex.
set (y := x \cap (substrate r)).
case: (emptyset_dichot y) => ye.
have xa: x = singleton a.
apply: set1_pr1 => //.
move=> z zx; move: (xs _ zx); rewrite sn; move /setU1_P.
case=>// => zr; empty_tac1 z; apply:setI2_i => //.
have ax: inc a x by rewrite xa; fprops.
exists a; red; aw;split => //.
rewrite xa => t /set1_P ->; apply /iorder_gleP; fprops.
by order_tac; apply: xs.
have sys:sub y (substrate r) by apply: subsetI2r.
move: (wo _ sys ye)=> [z []]; aw=> zy lez.
move: (setI2_1 zy) => zx.
exists z; split; aw => t tx; apply/iorder_gleP => //.
move: (xs _ tx); rewrite sn; case /setU1_P => p.
have ty: inc t y by rewrite /y; apply: setI2_i.
by move: (iorder_gle1 (lez _ ty)) => pa; apply:setU2_1.
rewrite p; move: gna=> [_]; apply; ue.
Qed.

Every set can be well-ordered; We assume here inc (rep a) a for any non-empty subset of E

Definition worder_of E :=
let p:= fun a => a -s1 (rep a) in
let chain:= fun F => [/\ sub F (powerset E), inc E F,
(forall A, inc A F -> inc (p A) F)
& (forall A, sub A F -> nonempty A -> inc (intersection A) F)] in
let om := intersection (Zo (powerset (powerset E)) chain) in
let d:= fun p => intersection (Zo om (fun x => sub p x)) in
let R := fun x => d (singleton x) in
graph_on (fun x y => (sub (R y) (R x))) E.

Lemma Zermelo_ter E: worder (worder_of E) /\ substrate (worder_of E) = E.
Proof.
rewrite /worder_of.
set p:= fun a => a -s1 (rep a).
set chain:= fun F => [/\ _,_, _ & _ ].
set om := intersection (Zo (powerset (powerset E)) chain).
set d:= fun p => intersection (Zo om (fun x => sub p x)).
set R := fun x => d (singleton x).
set res:= graph_on (fun x y => (sub (R y) (R x))) E.
have pe: p emptyset = emptyset by apply /set0_P => x /setC_P [/in_set0 xe _].
have sp: forall a, sub (p a) a by move=> t; apply:sub_setC.
have cp:chain (powerset E).
split; fprops; first by apply /setP_P.
move=> A /setP_P=> AE; apply/setP_P;apply: sub_trans AE; apply: sp.
move=> A AP [x xA]; move: (AP _ xA) => /setP_P xE; apply/setP_P.
move=> t ti; apply: xE; apply: (setI_hi ti xA).
have omv: om = intersection (Zo (powerset (powerset E)) chain) by done.
have co :chain om.
rewrite omv.
have aux: (nonempty (Zo (powerset (powerset E)) chain)).
by exists (powerset E); apply: Zo_i; aw; apply: setP_Ti.
split => //.
by apply:setI_s1; apply: Zo_i=> //; apply: setP_Ti.
by apply: (setI_i aux) =>y /Zo_hi [_].
move=> A Ai; apply:(setI_i aux) => y yi.
move: (yi)=> /Zo_hi [_ _ q _];apply: q;apply: (setI_hi Ai yi).
move=> A sAi neA; apply: (setI_i aux) => y yi.
move: (yi) => /Zo_hi [_ _ _]; apply => //.
by move=>t /sAi /setI_hi; apply.
move: (co)=> [sop Eo po io].
have cio: forall x, chain x -> sub om x.
move=> x xc; apply: setI_s1; apply: Zo_i =>//;apply /setP_P.
by move: xc => [].
pose m a:= forall x, inc x om -> sub x a \/ sub a x.
have am: om = Zo om m.
apply: extensionality; last by apply: Zo_S.
apply: (cio); split => //.
+ by apply: sub_trans sop; apply: Zo_S.
+ by apply: Zo_i=>//; move=> x xom; left;move: (sop _ xom); move/setP_P.
+ move=> A /Zo_P [Aom mA]; apply: Zo_i; first by apply: (po _ Aom).
suff aux: (sub om (Zo om (fun x=> sub x (p A) \/ sub A x))).
move=> x xom; case: (mA _ xom) => hyp.
move: (aux _ xom) => /Zo_hi; case =>xpB; first by left.
rewrite (extensionality xpB hyp); right; apply: sp.
right; apply: (sub_trans (sp A) hyp).
apply: cio; red; split.
- by apply: (@sub_trans om); first by apply: Zo_S.
- by apply: Zo_i=>//; right; move: (sop _ Aom);move/setP_P.
- move => B /Zo_P [Bom ors]; apply: Zo_i; first by apply: (po _ Bom).
case: ors => orsi; first by left; apply: sub_trans orsi; apply: sp.
case: (mA _ (po _ Bom)) => aux; last by right.
case: (inc_or_not (rep B) A)=> aux2.
rewrite (extensionality orsi _); first by left.
move=> t tB; case: (equal_or_not t (rep B)); first by move=> ->.
by move=> trB; apply: aux; apply/setC1_P; split.
right; move=> t tA;apply/setC1_P;split; [ by apply: orsi| dneg trB; ue].
- move=> B sB neB; apply: Zo_i.
apply: io =>//; apply: (sub_trans sB) ; apply: Zo_S.
case: (p_or_not_p (exists x, inc x B /\ sub x (p A))) => aux.
move: aux=> [x [xB xp]]; left; move=> t ti; apply: xp.
apply: (setI_hi ti xB).
right; move=> t tA; apply: setI_i=>//.
move=> y yB; move: (sB _ yB) => /Zo_P [yom ]; case; last by apply.
by move => sy; case: aux; exists y.
+ move=> A sAZ neA; apply: Zo_i.
apply: io =>//; apply: (sub_trans sAZ); apply: Zo_S.
move=> x xom.
case: (p_or_not_p (exists2 y, inc y A & sub y x)) => hyp.
move: hyp=> [y yA yx]; right; move => t ti.
apply: yx; apply: (setI_hi ti yA).
left; move=> t tx; apply: setI_i=>//.
move=> y yA; move: (sAZ _ yA)=> /Zo_P [yom my].
case: (my _ xom);[ by apply| move=> yx; case: hyp ;ex_tac; apply: Zo_S].
have st: forall a b, inc a om -> inc b om -> sub a b \/ sub b a.
move=> a b; rewrite {2} am; move => aom /Zo_P [bom ba]; apply: (ba _ aom).
have dpo: forall q, sub q E -> inc (d q) om.
by move=> q qE; rewrite /d; apply: io;[ apply:Zo_S| exists E;apply: Zo_i].
have pdp: forall q, sub q E -> sub q (d q).
rewrite /d=> q qE t tq; apply: setI_i; first by exists E; apply: Zo_i.
by move => y /Zo_hi; apply.
have dpq: forall q r, inc r om -> sub q r -> sub q E-> sub (d q) r.
by rewrite /d=> q r0 rom qr qE; apply: setI_s1; apply: Zo_i.
have rdq: forall q, sub q E -> nonempty q -> inc (rep (d q)) q.
move=> q qE neq; case: (inc_or_not (rep (d q)) q)=>// ni.
have aux: (sub q (p (d q))).
move=> t tq;apply /setC1_P; split; [ by apply: (pdp _ qE)|].
move => h;case: ni; ue.
move: (dpq _ _ (po _ (dpo _ qE)) aux qE).
rewrite /p; case: (emptyset_dichot (d q)).
move=> dqe; rewrite dqe pe in aux.
by move: neq=> [t tq]; case: (@in_set0 t); apply: aux.
move=> ned; move: (rep_i ned) => rd dc; move: (dc _ rd).
by move /setC1_P => [_].
have qdp: forall q r, inc r om -> sub q r -> inc (rep r) q -> r = d q.
move => q r rom qr rq.
have spE: sub q E by apply: (sub_trans qr); apply /setP_P; apply: sop.
move: (dpq _ _ rom qr spE) => sdqr.
case: (st _ _ (dpo _ spE) (po _ rom)) => ch.
by case /setC1_P: (ch _ ( (pdp _ spE) _ rq)) => _.
apply: extensionality =>// t tr.
case: (equal_or_not t (rep r)); first by move=> ->; apply: (pdp _ spE).
by move=> tnr; apply: ch; apply /setC1_P.
have Rp: forall x, inc x E ->
[/\ inc (R x) om, inc x (R x) & rep (R x) = x].
rewrite /R=> x xE.
have p1: sub (singleton x) E by apply: set1_sub.
have nesi: (nonempty (singleton x)) by fprops.
move: (rdq _ p1 nesi) => /set1_P => p3.
split; [ by apply: dpo | apply:(pdp _ p1); fprops | done].
have Ri:forall x y, inc x E -> inc y E -> R x = R y -> x = y.
move=> x y xE yE; move: (Rp _ xE)(Rp _ yE).
by move=> [_ _ p1][_ _ p2] p3; rewrite -p3 in p2; rewrite -p1 -p2.
have Rrq: forall q, inc q om -> nonempty q -> R (rep q) = q.
move=> a qom neq; rewrite /R; symmetry; apply: qdp =>//; last by fprops.
by move=> t /set1_P ->; apply: rep_i.
have sRR: forall x y, inc x E -> inc y E -> inc x (R y) -> (sub (R x) (R y)).
move=> x y xE yE xRy.
move: (Rp _ xE)(Rp _ yE) => [Rom xRx rR] [Rom' yRy rR'].
case: (st _ _ Rom Rom') =>// hyp.
move: (sub_set2 xRy yRy) => p1; move: (sub_trans p1 hyp) => p2.
have p3: (inc (rep (R x)) (doubleton x y)) by rewrite rR; fprops.
have p4: (inc (rep (R y)) (doubleton x y)) by rewrite rR'; fprops.
move: (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4).
move=> -> ->; fprops.
have -> : res = graph_on (fun x y => sub (R y) (R x)) E by done.
have or:order res.
rewrite /res; apply: order_from_rel1.
by move=> x y z /= xy yz; apply: sub_trans yz xy.
by move=> u v uE vE vu uv; apply: Ri=>//; apply: extensionality.
move => u ue; fprops.
have sr: substrate res = E.
rewrite /res graph_on_sr //; move => u ue; fprops.
split=>//;split=>//.
move=> x xsr nex; exists (rep (d x));red; rewrite -/res iorder_sr //.
rewrite sr in xsr.
move: (rdq _ xsr nex) => rdx; split => //.
move => a ax; apply/iorder_gleP => //; apply/graph_on_P1.
split => //;try apply: xsr=>//.
move: ((pdp _ xsr) _ ax)=> adx; apply: sRR; fprops.
have ne: (nonempty (d x)) by exists a.
by rewrite (Rrq _ (dpo _ xsr) ne).
Qed.

Two stricly increasing functions with the same range are equal if the source is well-ordered

Lemma strict_increasing_extens f g r r':
strict_increasing_fun f r r'-> strict_increasing_fun g r r' -> worder r ->
range (graph f) = range (graph g) -> f = g.
Proof.
move=> sif sig wo.
have to: total_order r by apply: worder_total.
have sm: (strict_monotone_fun f r r') by left.
have smg: (strict_monotone_fun g r r') by left.
move: (total_order_monotone_injective to sm)=> injf.
move: (total_order_monotone_injective to smg)=> injg {sm smg}.
move:sif sig=> [or or' [ff sr sr'] si] [_ _ [fg srg sr'g] sig] rr.
set (A:=Zo (source f)(fun x=> Vf f x <> Vf g x)).
case: (emptyset_dichot A) => eA.
apply: function_exten=>//; try ue.
by move=> x xsf; ex_middle sg; empty_tac1 x;rewrite /A; apply: Zo_i.
have Asf: (sub A (substrate r)) by rewrite- sr /A;apply: Zo_S.
move:wo=> [_ wo]; move: (wo _ Asf eA)=> [x []]; aw => xA xl.
have xsf: inc x (source f) by rewrite sr; apply: Asf.
have xsg: inc x (source g) by rewrite srg - sr.
have: inc (Vf f x) (range (graph g)) by rewrite -rr; apply: Vf_range_g.
move/(range_fP fg) => [y ysg WW].
move:(ysg); rewrite srg - sr=> ysf.
have: inc (Vf g x ) (range (graph f)) by rewrite rr; apply: Vf_range_g.
move/(range_fP ff) => [z zsf WWw].
move:(zsf); rewrite sr - srg=> zsg.
have xsr: inc x (substrate r) by apply: Asf.
have ysr: inc y (substrate r) by rewrite srg in ysg.
have zsr: inc z (substrate r) by rewrite sr in zsf.
have p1: glt r' (Vf g x) (Vf f x).
have a0: x <> y by move=> h; move: xA WW; rewrite -h; move /Zo_P => [].
rewrite WW; case: (total_order_pr1 to xsr ysr) => // h;first by apply: sig.
move: (sig _ _ h) => [le ne].
suff: inc y A by move=> h'; move:(iorder_gle1 (xl _ h'))=> h''; order_tac.
by apply: Zo_i=>//;rewrite -WW => aux;case: a0; symmetry; apply: (proj2 injf).
have p2: glt r' (Vf f x) (Vf g x).
have a0: x <> z by move=> h; move: xA WWw;rewrite -h;move /Zo_P => []; fprops.
rewrite WWw; case: (total_order_pr1 to xsr zsr) => h //; first by apply: si.
move: (si _ _ h) => [le ne].
suff: inc z A by move=> h'; move:(iorder_gle1 (xl _ h'))=> h''; order_tac.
apply: Zo_i=>//.
by rewrite -WWw; clear ne; dneg xx; move: injg=> [_ p]; apply: p.
order_tac.
Qed.

A segment is a set such that if if contains x, it contains all elements less than x. Left-unbounded intervals are segments.

Definition segmentp r s :=
sub s (substrate r) /\ forall x y, inc x s -> gle r y x -> inc y s.
Definition segment r s := interval_uo r s.
Definition segmentc r s := interval_uc r s.

Lemma lt_in_segment r s x y:
segmentp r s -> inc x s -> glt r y x -> inc y s.
Proof. move=> [ss sp] xs [le ne]; apply: sp xs le. Qed.

Lemma inc_segment r x y:
inc y (segment r x) -> glt r y x.
Proof. by move /Zo_hi. Qed.

Lemma not_in_segment r x: inc x (segment r x) -> False.
Proof. by move=> h; move: (inc_segment h) =>[_ h']. Qed.

Lemma sub_segment r x: sub (segment r x) (substrate r).
Proof. by move=> t /Zo_P; case. Qed.

Lemma sub_segment1 r s: segmentp r s -> sub s (substrate r).
Proof. by move=> [ss sp] t ts; apply: ss.
Qed.

Lemma sub_segment2 r x y:
sub (segment (induced_order r x) y) x.
Proof.
move=> t /Zo_hi [ h _]; move: h;rewrite /induced_order => h.
by move: (setI2_2 h) => /setXp_P [].
Qed.

Lemma segment_inc r x y:
glt r y x -> inc y (segment r x).
Proof. move=> xy;apply /Zo_P; split=>//;order_tac. Qed.

Lemma segmentP r x y:
inc y (segment r x) <-> glt r y x.
Proof. by split; [ apply: inc_segment | apply: segment_inc]. Qed.

Lemma segmentcP r x y:
inc y (segmentc r x) <-> gle r y x.
Proof.
split; [ by move/Zo_P => [] | move =>h;apply: Zo_i =>//; order_tac ].
Qed.

Lemma inc_bound_segmentc r x: order r -> inc x (substrate r) ->
inc x (segmentc r x).
Proof. by move=> or xs;apply/segmentcP =>//; order_tac. Qed.

Lemma sub_segmentc r x: sub (segmentc r x) (substrate r).
Proof. by move=> t /Zo_P []. Qed.

Hint Resolve inc_bound_segmentc: fprops.

Lemma segmentc_pr r x: order r -> inc x (substrate r) ->
(segment r x) +s1 x = segmentc r x.
Proof.
move=> or xsr;set_extens y.
case /setU1_P; first by move/segmentP => [pa _]; apply/segmentcP.
by move =>-> ; apply inc_bound_segmentc.
move/segmentcP => h; case: (equal_or_not y x)=> h1.
by apply/setU1_P; right.
by apply/setU1_P; left; apply/segmentP; split.
Qed.

Examples of segments. Empty set, whole substrate, union, intersection, subsegments

Lemma set0_segment r: segmentp r emptyset.
Proof. by split; [ fprops | move=> x y /in_set0 ]. Qed.

Lemma substrate_segment r: order r -> segmentp r (substrate r).
Proof. move=> or; split => // x y xst xy; order_tac. Qed.

Lemma segment_segment r x: order r ->
inc x (substrate r) -> segmentp r (segment r x).
Proof.
move=> or xs; rewrite /segment/interval_uo.
split; first by apply: Zo_S.
move=> a b /Zo_P [asr ax] ba; apply: Zo_i; order_tac.
Qed.

Lemma segmentc_segment r x:
order r -> inc x (substrate r) ->
segmentp r (segmentc r x).
Proof.
move=> or xs; split; first by apply: Zo_S.
move=> a b /Zo_P [asr ax] ba; apply: Zo_i; order_tac.
Qed.

Lemma subsegment_segment r s s': order r ->
segmentp r s -> segmentp (induced_order r s) s' -> segmentp r s'.
Proof.
move=> or srs sis.
move: (sub_segment1 srs)=>ssr.
red; move: sis; rewrite /segmentp; aw.
move=> [s's hyp]; split.
by apply: sub_trans s's ssr.
move=> x y xs' yx; move: (s's _ xs')=> xs; move: srs=> [_ h].
apply: (hyp _ _ xs'); apply /iorder_gleP => //; apply: h xs yx.
Qed.

Lemma setI_segment r s: order r -> nonempty s ->
(alls s (segmentp r)) -> segmentp r (intersection s).
Proof.
move=> or nes als; split.
move :nes => [y ys] x xs; move: (als _ ys) => [yss _].
exact (yss _ (setI_hi xs ys)).
move=> x y xi yx; apply: (setI_i nes).
move=> z zs; move: (als _ zs) => [_ p].
apply : p (setI_hi xi zs) yx.
Qed.

Lemma setUf_segment r j s: order r ->
(alls j (fun x => segmentp r (s x))) -> segmentp r (unionf j s).
Proof.
move=> or als; split.
move=> t tu;move: (setUf_hi tu)=> [y yj ts].
by move:(als _ yj) => [ss _]; apply: ss.
move=> x y xu xy;move: (setUf_hi xu)=> [z zj ts].
move:(als _ zj) => [_ ss]; move: (ss _ _ ts xy) =>h.
union_tac.
Qed.

Lemma setU_segment r s: order r ->
(alls s (segmentp r))-> segmentp r (union s).
Proof.
move=> or als; rewrite setU_prop; apply: setUf_segment => //.
Qed.

Any segment is segment r x or the whole set

Theorem well_ordered_segment r s: worder r -> segmentp r s ->
s = substrate r \/ (exists2 x, inc x (substrate r)& s = segment r x).
Proof.
move=> wor sr.
case: (equal_or_not s (substrate r));[by left | move=> snr; right].
set (y:= (substrate r) -s s).
have ney: nonempty y.
by move: sr=> [sr _] ; apply: setC_ne; split.
move: (worder_total wor) => tor.
have sys: (sub y (substrate r)) by apply: sub_setC.
move:wor=> [or wo]; move: (wo _ sys ney)=> [x []]; aw.
move=> xy xle.
have xis: inc x (substrate r) by apply: sys.
ex_tac;set_extens z => zs.
apply/segmentP.
have zsr: inc z (substrate r) by apply: (sub_segment1 sr).
case: (total_order_pr2 tor zsr xis) => //.
case /setC_P: xy => [_ bad].
by move: sr=> [_ h] xz; move: (h _ _ zs xz ).
ex_middle zis.
have zy: (inc z y) by apply/setC_P; split => // ;apply: (sub_segment zs).
move: (iorder_gle1 (xle _ zy)) (inc_segment zs)=> p1 p2; order_tac.
Qed.

Lemma segment_alt r x a: order r -> least r a ->
segment r x = interval_co r a x.
Proof.
move => or [ais lea]; set_extens t; move /Zo_P => [pa pb]; apply/Zo_P;fprops.
by move: pb => [_].
Qed.

Lemma segment_alt1 r s: worder r -> segmentp r s ->
s = substrate r \/ (exists x, exists a, s = interval_co r a x).
Proof.
move => wo iss.
case: (emptyset_dichot (substrate r)) => sre.
left; move: iss=> [p _].
apply: extensionality=>//;rewrite sre; fprops.
case: (well_ordered_segment wo iss); first by left.
move=> [x xsr p].
move: (worder_least wo sre)=> [a lea].
right; exists x; exists a; rewrite - segment_alt //.
by move: wo=> [].
Qed.

Lemma segment_monotone r x y: order r -> gle r x y ->
sub (segment r x) (segment r y).
Proof.
move=> or xy t ts; move: (inc_segment ts) => h.
apply: segment_inc; order_tac.
Qed.

Lemma segment_dichot_sub r x y:
worder r -> segmentp r x -> segmentp r y ->
(sub x y \/ sub y x).
Proof.
move=> wo sx sy.
case: (well_ordered_segment wo sx).
by move=> ->; right; apply: sub_segment1.
move=> [a ar xsa];case: (well_ordered_segment wo sy).
by move=> ->; left; apply: sub_segment1.
move=>[b br ysb].
move:(worder_total wo) => [or h].
by rewrite xsa ysb;case: (h _ _ ar br); [left | right]; apply: segment_monotone.
Qed.

Lemma le_in_segment r x y z: order r -> inc x (substrate r) ->
inc y (segment r x) -> gle r z y -> inc z (segment r x).
Proof.
move=> or xsr ysr zy; apply: segment_inc=>//.
move: (inc_segment ysr)=> aux; order_tac.
Qed.

Lemma coarse_segment_monotone r x y: order r -> gle r x y ->
sub (coarse (segment r x)) (coarse (segment r y)).
Proof.
by move=> or xy;move: (segment_monotone or xy) =>sm; apply: setX_Slr.
Qed.

Lemma segment_induced_a r s x:
order r -> segmentp r s -> inc x s ->
segment (induced_order r s) x = segment r x.
Proof.
move=> or srs xs; set_extens t=> ys.
move: (inc_segment ys)=> iys; move: (iorder_gle2 iys)=> tx.
apply: segment_inc=>//; order_tac.
apply: segment_inc.
move: (inc_segment ys)=> [tx nxy]; split => //; apply /iorder_gleP=> //.
apply (proj2 srs _ _ xs tx).
Qed.

Lemma segment_induced r a b: order r -> glt r b a ->
segment (induced_order r (segment r a)) b = segment r b.
Proof.
move=> or ab.
have h: inc a (substrate r) by order_tac.
rewrite segment_induced_a //; last by apply /segmentP.
apply: segment_segment=>//.
Qed.

Lemma segment_induced1 r a b: order r -> glt r b a ->
segment (induced_order r (segmentc r a)) b = segment r b.
Proof.
move=> or ab.
have h: inc a (substrate r) by order_tac.
rewrite segment_induced_a =>//; last by apply/segmentcP; order_tac.
apply: segmentc_segment=>//.
Qed.

The union of all segments of E, distinct from E, is E when it has no gratest element, E minus its greatest element otherwise. Assumes the set totally ordered

Definition segmentss r:=
fun_image (substrate r) (segment r).

Lemma union_segments r: total_order r ->
let E := substrate r in
let A := union (segmentss r) in
( (forall x, ~ (greatest r x)) -> A = E)
/\ (forall x, greatest r x -> A = E -s1 x).
Proof.
move=> tor E A.
have Ap: forall x, inc x A <-> exists y, glt r x y.
move=> x;split.
move/setU_P => [y xy /funI_P [z zE sy]].
exists z; apply: inc_segment;ue.
move=> [y xy]; apply/setU_P;exists (segment r y).
by apply: segment_inc=>//; order_tac.
apply/funI_P; exists y => //; rewrite /E; order_tac.
have AE: sub A E by move=> t /Ap [y xy]; rewrite /E;order_tac.
split.
move=> p; apply: extensionality=>// t tE.
apply /Ap; ex_middle bad; case: (p t); split =>//.
move=> y ysr; case: (total_order_pr2 tor tE ysr)=>//.
by move=> ty; case: bad; exists y.
move=> x [xs gr]; set_extens y => ys.
apply/setC_P;split; first by apply: AE.
move=> /set1_P xy; move: ys; rewrite Ap; move=> [z yz].
have zc: inc z (substrate r) by order_tac.
move: (gr _ zc) => aux.
rewrite xy in yz; move:tor=> [or _];order_tac.
move /setC_P: ys => [yE] /set1_P yx.
apply/Ap; exists x; split=>//; by apply: gr.
Qed.

The mapping that associates to each x the segment with endpoint x is a bijection from E to the set of segments of E, different from E. It is an order isomorphism (target ordered by inclusion), for any well-ordering. The set of all segments is thus well-ordered

Definition segments r:=
(segmentss r) +s1 (substrate r).
Definition segments_iso r:=
Lf (segment r) (substrate r) (segmentss r).

Lemma inc_segmentsP r: worder r -> forall x,
(segmentp r x <-> inc x (segments r)).
Proof.
move => wor x; split=> hyp.
case: (well_ordered_segment wor hyp).
by move => ->; apply /setU1_P; right.
move=> [y ysr ->]; apply /setU1_P; left; apply/funI_P; ex_tac.
move:wor=> [or wor].
case /setU1_P: hyp.
move/funI_P => [z zr ->]; apply: segment_segment=>//.
by move=> ->; apply: substrate_segment.
Qed.

Lemma segment_insetof r x: worder r -> inc x (substrate r) ->
inc (segment r x) (segments r).
Proof.
move=> wo xsr; apply/(inc_segmentsP wo).
apply: segment_segment; fprops.
Qed.

Lemma segmentc_insetof r x: worder r -> inc x (substrate r) ->
inc (segmentc r x) (segments r).
Proof.
move=> wo xsr; apply/(inc_segmentsP wo).
apply: segmentc_segment; fprops.
Qed.

Lemma sub_segments r x: worder r ->
inc x (segments r) -> sub x (substrate r).
Proof.
move=> wor /(inc_segmentsP wor) ;apply: sub_segment1.
Qed.

Lemma segment_monotone1 r x y: total_order r ->
inc x (substrate r) -> inc y (substrate r) ->
sub (segment r x)(segment r y) -> gle r x y.
Proof.
move=> tor xsr ysr sxy.
case: (total_order_pr2 tor ysr xsr)=>//.
by move/segmentP=> yis; move: (sxy _ yis) => /segmentP [].
Qed.

Lemma segment_injective r x y: total_order r ->
inc x (substrate r) -> inc y (substrate r) -> segment r x = segment r y ->
x = y.
Proof.
move=> tor xsr ysr sxy.
have p1: (sub (segment r x)(segment r y)) by rewrite sxy.
have p2: (sub (segment r y)(segment r x)) by rewrite sxy.
move: (segment_monotone1 tor xsr ysr p1)=> p3.
move: (segment_monotone1 tor ysr xsr p2)=> p4.
move: tor=> [or _]; order_tac.
Qed.

Theorem segments_iso_is r: worder r ->
order_isomorphism (segments_iso r) r (sub_order (segmentss r)).
Proof.
move=> wor;move: (wor)=> [or worp].
have ta: lf_axiom (segment r) (substrate r) (segmentss r).
by move => t ts; apply /funI_P; ex_tac.
move: (sub_osr (segmentss r)) => [pa pb].
red; rewrite /segments_iso;split => //.
split; aw => //;apply: lf_bijective=> //.
move=> u v; apply: (segment_injective (worder_total wor)).
move=> y /funI_P [z za ->];ex_tac.
red; aw; move=> x y xsr ysr; aw; split.
move=> hyp; apply/sub_gleP;split => //; fprops.
by apply: segment_monotone.
move /sub_gleP=> [_ _ ss].
by apply: segment_monotone1=>//; apply: worder_total.
Qed.

Theorem segments_worder r: worder r ->
worder (sub_order (segments r)).
Proof.
move=> wor; move: (wor)=> [or worp];move: (worder_total wor)=> tor.
move: (sub_osr (segments r)) => [oi sr].
split=>//.
rewrite sr; move => x xsr nex.
set y := x \cap (segmentss r).
move: (xsr); rewrite -{1} sr => h.
rewrite /least (proj2 (iorder_osr oi h)); clear h.
case: (emptyset_dichot y) => hy.
have xs: x = singleton (substrate r).
apply: set1_pr1=>// z zx.
move: (xsr _ zx); case /setU1_P => //.
by move=> aux; empty_tac1 z; apply: setI2_i.
exists (substrate r); rewrite xs; split; fprops.
move=> z => /set1_P ->;apply /iorder_gleP; fprops; order_tac.
rewrite sr; apply: xsr; rewrite xs; fprops.
have ysr: (sub y (segmentss r)) by move => t ty; apply (setI2_2 ty).
have segp: (forall a, inc a y -> exists2 u,
inc u (substrate r) & a = segment r u).
by move=> a ay; move: (ysr _ ay) => /funI_P.
pose cf a := select(fun u => a = segment r u) (substrate r).
have cfp: forall a, inc a y ->
(inc (cf a) (substrate r) /\ a = segment r (cf a)).
move=> a ay; move: (segp _ ay) => [u us uv].
suff : u = cf a by move => <-; split => //.
apply: (select_uniq _ us uv); move => c b csr sc bsr sb.
by apply: (segment_injective (worder_total wor) csr bsr); rewrite - sb - sc.
set (z:= fun_image y cf).
have nez: nonempty z by move:hy=> [w wy];exists (cf w); apply/funI_P; ex_tac.
have zsr: sub z (substrate r).
by move => t /funI_P [u uy ->]; move: (cfp _ uy)=> [res _].
move: (worp _ zsr nez)=> [a []]; aw=> asr lea.
have sax: (inc (segment r a) x).
move: asr => /funI_P [u uy ->].
move: (cfp _ uy)=> [h <-]; apply: (setI2_1 uy).
ex_tac;move=> b bx; apply /iorder_gleP; (try apply: xsr) => //.
move: (xsr _ bx) => pa.
apply /sub_gleP;split; fprops.
case /setU1_P: pa; last by move=>->; apply: sub_segment.
move=> h.
have biy: (inc b y) by apply: setI2_i.
have cbz: (inc (cf b) z) by apply /funI_P; ex_tac.
move: (iorder_gle1 (lea _ cbz)).
move: (cfp _ biy)=> [p1 p2]; rewrite {2} p2.
apply: segment_monotone=>//.
Qed.

Assume that G is a family such that (a) each G(i) is a well-ordering on E(i); (b) if E(i) is a subset of E(j), then G(j) agrees with G(i) on E(i), and (c) for any i and j there is k such that E(k) is a subset of E(i) and E(j). Instead of (c) we may assume (d) that one E(i) of E(j) is a segment of the order.
Then the union of G is a well-ordering; moreover segments of the union are segments of G(i).

Definition worder_fam g := allf g worder.
Definition order_extends r r' := r = induced_order r' (substrate r).
Definition monotone_order_fam g :=
forall a b, inc a (domain g) -> inc b (domain g) ->
sub (substrate (Vg g a)) (substrate (Vg g b)) ->
order_extends (Vg g a) (Vg g b).

Definition common_extension_order g h:=
[/\ order h, substrate h = unionf (domain g) (fun a => substrate (Vg g a))
& (forall a, inc a (domain g) -> order_extends (Vg g a) h)].

Definition common_extension_order_axiom g :=
[/\ order_fam g,
(forall a b, inc a (domain g) -> inc b (domain g )-> exists c,
[/\ inc c (domain g), sub (substrate (Vg g a)) (substrate (Vg g c))
& sub (substrate (Vg g b)) (substrate (Vg g c))])
& monotone_order_fam g].
Definition common_worder_axiom g:=
[/\ worder_fam g,
(forall a b, inc a (domain g) -> inc b (domain g) ->
segmentp (Vg g a) (substrate (Vg g b))
\/ segmentp (Vg g b) (substrate (Vg g a)))
& monotone_order_fam g].

We first show that we have an ordering that extends G(i)

Lemma order_merge1 g:
common_extension_order_axiom g -> common_extension_order g (unionb g).
Proof.
set G := (unionb g); move=> [alo eVVg pVV].
have gu: sgraph G.
move=> t tu; move: (setUb_hi tu)=> [x xdg xp].
by move: (alo _ xdg); fprops=> h; apply: (order_sgraph h).
set (E:=unionf (domain g) (fun a : Set => substrate (Vg g a))).
have ur: forall y,inc y E -> related (unionb g) y y.
rewrite /E=> y yE; move: (setUf_hi yE)=> [x xdg xp].
by move: (alo _ xdg); fprops=> h; apply: (setUb_i xdg); order_tac.
have su: substrate G = E.
set_extens x; last by move=> xE; move: (ur _ xE)=> h; substr_tac.
rewrite /E;case /(substrate_P gu) => [] [y Ju];
move: (setUf_hi Ju)=> [z zdg zp]; union_tac;
move: (alo _ zdg)=> h; substr_tac.
have cov: forall x y, inc x G -> inc y G ->
exists u, [/\ inc u (domain g), inc x (Vg g u)& inc y (Vg g u)].
move=> x y xu yu.
move: (setUf_hi xu) (setUf_hi yu)=> [a adg ap][b bdg bp].
move: (eVVg _ _ adg bdg)=> [c [cdg sac sbc]].
move:(pVV _ _ adg cdg sac)(pVV _ _ bdg cdg sbc)=> Vag Vbg.
move: ap bp; rewrite Vag Vbg /induced_order; aw.
by move /setI2_P => [p1 _] /setI2_P [p2 _]; exists c.
have oG: order G.
split => //.
by red; rewrite su.
rewrite /related; move=> x y z p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
move: (alo _ cdg) => or; rewrite /G; red; union_tac; order_tac.
rewrite /related; move=> x y p1 p2.
move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
move: (alo _ cdg)=> or; order_tac.
split=>// a adg;set_extens x => xs.
apply/setI2_P; split; first by rewrite /G; union_tac.
move: (alo _ adg)=> [ga _ _ _].
by move:(sub_graph_coarse_substrate ga); apply.
move: (setUb_hi (setI2_1 xs))=> [z zdg zpr].
move: (eVVg _ _ adg zdg)=> [t [tdg sa sz]].
rewrite (pVV _ _ adg tdg sa); apply/setI2_P;split;last by apply: (setI2_2 xs).
by move: zpr; rewrite(pVV _ _ zdg tdg sz); move/setI2_P => [].
Qed.

There is at most one extension

Lemma order_merge2 g: common_extension_order_axiom g ->
uniqueness (common_extension_order g).
Proof.
move => [alo eVVg pVV] h1 h2 c1 c2.
suff: (forall h1 h2, common_extension_order g h1 ->
common_extension_order g h2 -> sub h1 h2).
by move=> aux; apply: extensionality; apply: aux.
move => r r' [or sr vr][or' sr' vr'].
move=> x xr.
have ppx: pairp x by move: or=>[gr _ _ _]; apply: gr.
have px: J (P x) (Q x) = x by aw.
have pxs: (inc (P x) (substrate r)) by substr_tac.
have pys: (inc (Q x) (substrate r)) by substr_tac.
rewrite sr in pxs pys.
move: (setUf_hi pxs) (setUf_hi pys)=> [u udg psu][v vdg qsv].
move:(eVVg _ _ udg vdg)=> [w [wdg wu wv]].
have: (inc x (Vg g w)).
rewrite (vr _ wdg); apply /setI2_i => //;apply/setX_P;split;fprops.
by rewrite (vr' _ wdg) ; move /setI2_P => [].
Qed.

Property (d) implies (c); in this case, the unique extension is the union

Lemma order_merge3 g:
common_worder_axiom g -> common_extension_order_axiom g.
Proof.
move=> [alwo pa pb];split => //.
by move => w xdg; move: (alwo _ xdg) => [ok _].
move => a b adg bdg;case: (pa _ _ adg bdg); rewrite /segmentp;
move => [ss _]; [ exists a | exists b]; split=> //.
Qed.

Lemma order_merge4 g:
common_worder_axiom g -> common_extension_order g (unionb g).
Proof. by move=> ga; apply: order_merge1; apply: order_merge3. Qed.

Lemma order_merge5 g: common_worder_axiom g ->
uniqueness (common_extension_order g).
Proof.
move=> ca h1 h2 a1 a2;apply: (order_merge2 (order_merge3 ca) a1 a2).
Qed.

This is the main result

Theorem worder_merge g (G := unionb g):
common_worder_axiom g ->
[/\ (common_extension_order g G),
worder G,
(forall a x, inc a (domain g) -> segmentp (Vg g a) x
-> segmentp G x),
(forall a x, inc a (domain g) -> inc x (substrate (Vg g a)) ->
segment (Vg g a) x = segment G x)
& (forall x, segmentp G x ->
x = substrate G \/ exists2 a, inc a (domain g) & segmentp (Vg g a) x)].
Proof.
move=> co.
move: (order_merge4 co)=>coe.
move: coe=> [oh sh Vag].
move: co => [pb pc pd].
have p1: (forall a, inc a (domain g) -> sub (substrate (Vg g a)) (substrate G)).
by move=> a adg; rewrite sh; move=> t ts; apply: (setUf_i adg).
have p2: (forall a, inc a (domain g) -> segmentp G (substrate(Vg g a))).
move=> a adg;split; first by apply: p1.
move=> x y xs yx.
have ys: (inc y (substrate G)) by order_tac.
move: (setUf_hi yx) => [ u udg Jv].
case: (pc _ _ adg udg); move=> [p p']; first by apply: p; substr_tac.
apply: (p' _ _ xs Jv).
have p3:(forall a x, inc a (domain g) -> inc x (substrate (Vg g a))
-> segment (Vg g a) x = segment G x).
move=> a x adg xs; set_extens y => ys; move: (inc_segment ys) => [yx nyx].
apply /segmentP; split=>//; apply: setUb_i adg yx.
apply/segmentP; split => //.
move: (setUf_hi yx)=> [b bdg Jv]; rewrite (Vag _ adg).
apply/iorder_gleP => //.
case:(pc _ _ adg bdg); move=> [p p']; first by apply: p; substr_tac.
apply: (p' _ _ xs Jv).
have p4: (forall a x, inc a (domain g) -> segmentp (Vg g a) x ->
segmentp G x).
by move=> ->; apply: p2.
move=> [y ysV ->]; rewrite (p3 _ _ adg ysV); apply: segment_segment=>//.
have p5: worder G.
split=>//; move=> x xsr [y yx].
move: (xsr _ yx)=> ysr; rewrite sh in ysr.
move: (setUf_hi ysr) => [a adg ysVa].
set (x1:= x \cap (substrate (Vg g a))).
have sx1s: (sub x1 (substrate (Vg g a))) by apply: subsetI2r.
have nx1: nonempty x1 by exists y; apply: setI2_i.
move: (wo _ sx1s nx1)=> [z []]; aw => zs zle.
have zx: inc z x by apply: (setI2_1 zs).
have zVa: inc z (substrate (Vg g a)) by apply: (setI2_2 zs).
exists z; red; aw; split=> //.
move=> t tx; apply/iorder_gleP => //.
move: (xsr _ tx); rewrite sh => tu; move: (setUf_hi tu)=> [b bdg bV].
have aux: inc t (substrate (Vg g a)) -> gle (unionb g) z t.
move=> hyp.
have tx1: inc t x1 by apply: setI2_i.
move:(iorder_gle1 (zle _ tx1)); rewrite Vag // => h.
by move:(iorder_gle1 h).
case: (pc _ _ adg bdg); move => [p p']; first by apply: (aux (p _ bV)).
move: (p _ zVa)=> zVb.
case: (total_order_pr2 (worder_total (pb _ bdg)) bV zVb).
move=> [tz ntz]; apply: (aux (p' _ _ zVa tz)).
rewrite Vag // => h; exact:(iorder_gle1 h).
split => //.
move=> x seg.
case: (well_ordered_segment p5 seg); [ by left | move=>[y ysr ->]; right ].
rewrite sh in ysr; move: (setUf_hi ysr)=> [a adg ap]; ex_tac.
rewrite -(p3 _ _ adg ap); apply: segment_segment => //.
Qed.

## EIII-2-2 The principle of transfinite induction

Let O(x) and C(x) be the set of all elements less than (resp. less or equal than) x. These are segments, and C(x) is the union of O(x) and the singleton x. In a well-ordered set every segment S is of the form C(x) or the union of all segments of S, distinct from S. Consequence: a set of segments, stable by union, and stable by the mapping O->C contains all segments.

Section TransfinitePrinciple.
Variables r s: Set.
Hypothesis wor: worder r.
Hypothesis u_stable: forall s', sub s' s -> inc (union s') s.
(forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segmentc r x) s).

Lemma transfinite_principle1 x: segmentp r x -> inc x s.
Proof.
move=> sx.
have or: order r by move: wor=> [].
move: (segments_worder wor) => woi.
set (cs:= (segments r) -s s).
case: (emptyset_dichot cs) => necs.
have nc: (~ inc x cs) by rewrite necs; case; case.
move: sx => /(inc_segmentsP wor) sx.
apply: (nin_setC sx nc).
have scs: sub cs (segments r) by rewrite /cs; apply: sub_setC.
move:(proj2 (sub_osr (segments r))) => sr1.
move: woi=> []; rewrite sr1 => oi woi.
move: (woi _ scs necs).
move: (scs); rewrite - {1} sr1 => src1.
move=> [y []]; rewrite (proj2 (iorder_osr oi src1));move=> ycs hyp; clear woi.
move: (scs _ ycs)=> yssr.
have nys: ~ (inc y s).
move: ycs => / setC_P [_]; apply.
have ysr:(sub y (substrate r)) by apply: sub_segments=>//.
have woi: worder (induced_order r y) by apply: induced_wor.
case: (p_or_not_p (exists a, greatest (induced_order r y) a)).
move=> [a []]; aw => [ay pa].
move: (ysr _ ay)=> asr.
have ysc: (y = segmentc r a).
set_extens t => ts; first by move: (iorder_gle1 (pa _ ts)) => /segmentcP.
move: ts => /segmentcP ta.
move: yssr => /(inc_segmentsP wor) [_ aux]; apply: (aux _ _ ay ta).
case: (p_or_not_p (inc (segment r a) cs))=> h.
move: (iorder_gle1 (hyp _ h)) => /sub_gleP [_ _ ysa].
case: (not_in_segment (ysa _ ay)).
have p1: (inc (segment r a) (segments r)) by apply: segment_insetof.
by case: nys; rewrite ysc; apply: adj_stable =>//; apply: (nin_setC p1 h).
move=> nge.
have aux: (forall x : Set, ~ greatest (induced_order r y) x).
by move=> b ngeb; case: nge; exists b.
move: (union_segments (worder_total woi))=> [unm _].
move: (unm aux); aw => us; clear aux unm.
case: nys; rewrite -us; apply: u_stable.
move => z /funI_P [u uy zv].
case: (inc_or_not z cs) => zcs.
move:(iorder_gle1 (hyp _ zcs)) => /sub_gleP [_ _ yz].
move: uy; aw => uy; move: (yz _ uy).
rewrite zv=> aux; case: (not_in_segment aux).
have siu: (segmentp (induced_order r y) z).
rewrite zv; apply: segment_segment; fprops; aw.
have zsr: (inc z (segments r)).
apply /(inc_segmentsP wor).
move: yssr => /(inc_segmentsP wor) yssr.
apply: (subsegment_segment or yssr siu).
by apply: (nin_setC zsr zcs).
Qed.

Lemma transfinite_principle2: inc (substrate r) s.
Proof.
apply: (transfinite_principle1); apply: substrate_segment; fprops.
Qed.

End TransfinitePrinciple.

Two proofs of the transfinite principle; either by application of the previous lemma or direct proof (in ssete2)

Theorem transfinite_principle r (p:property):
worder r ->
(forall x, inc x (substrate r) ->
(forall y, inc y (substrate r) -> glt r y x -> p y) -> p x) ->
forall x, inc x (substrate r) -> p x.
Proof.
move => wor hyp x xsr.
have or: order r by move: wor=> [or _].
set (s:= Zo (segments r)(fun z => forall y, inc y z -> p y)).
have alseg: forall x, inc x s -> segmentp r x.
by move=> t /Zo_P [] /(inc_segmentsP wor).
have su:forall s', sub s' s -> inc (union s') s.
move=> s' s's; apply /Zo_P; split.
apply /(inc_segmentsP wor);apply: setU_segment =>//.
by move=> t ts'; apply: alseg; apply: s's.
move=> y yu; move: (setU_hi yu)=> [v yv vs].
by move: (s's _ vs) => /Zo_hi; apply.
have seg: forall x, inc x (substrate r) -> inc (segment r x) s ->
inc (segmentc r x) s.
move=> y ysr yxs; rewrite /s; apply: Zo_i.
apply /(inc_segmentsP wor); apply: segmentc_segment =>//.
move: yxs => /Zo_P [p1 p2].
move=> z; rewrite - segmentc_pr //; case /setU1_P; first by apply: p2.
move=> ->; apply: hyp =>//; move=> t tsr ty; apply: p2; fprops.
by apply: segment_inc.
move: (transfinite_principle2 wor su seg).
by move => /Zo_hi; apply.
Qed.

Let r be a well-ordering, x in the substrate, S(x) the segment with endpoint x, and g a function, whose source contains S(x). We define gx to be the restriction of g to Sx; and study some properties.

Definition restriction_to_segment r x g :=
restriction1 g (segment r x).

Lemma rts_fs r x g: function g -> sub (segment r x) (source g)
-> surjection (restriction_to_segment r x g).
Proof. by move=> p3 p4; apply: restriction1_fs. Qed.

Lemma rts_extensionality r s x f g:
segment r x = segment s x ->
function f -> sub (segment r x) (source f) ->
function g -> sub (segment s x) (source g) ->
{inc (segment r x), f =1f g} ->
restriction_to_segment r x f = restriction_to_segment s x g.
Proof.
move=> srsx ff srf fg ssg sv.
have pa: source (restriction_to_segment r x f) = segment r x.
rewrite /restriction_to_segment/restriction1; aw.
apply: function_exten4.
rewrite /restriction_to_segment /restriction1; aw.
by apply restriction1_fs.
by apply restriction1_fs.
rewrite pa => t ts.
rewrite (restriction1_V ff srf ts) (sv _ ts).
by rewrite srsx in ts; rewrite (restriction1_V fg ssg ts).
Qed.

A function f is defined by transfinite induction by p if f(x) is p(fx), where fx is as above. It exists, its graph is unique. The value f(x) is in a set F if, for all g whose source is a segment and target is a subset of F, p(g) is in F. We start with some uniqueness properties

Definition transfinite_def r (p: fterm) f :=
[/\ surjection f, source f = substrate r &
forall x, inc x (substrate r) -> Vf f x = p (restriction_to_segment r x f)].

Lemma transfinite_unique1 r p f f' z:
transfinite_def r p f -> transfinite_def r p f' ->
{inc (segment r z), f =1f f'} ->
restriction_to_segment r z f = restriction_to_segment r z f'.
Proof.
move=> [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW.
have ss: sub (segment r z) (substrate r) by apply: sub_segment.
apply: rts_extensionality => //; ue.
Qed.

Lemma transfinite_unique r p : worder r ->
uniqueness (transfinite_def r p).
Proof.
move=> wo f f' tf tf'.
set (s:=Zo(segments r) (fun z => {inc z, f =1f f'})).
move: (wo)=> [or _].
have alse:forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(inc_segmentsP wo).
have su: forall s', sub s' s -> inc (union s') s.
move=> s' s's; apply /Zo_P; split.
apply/(inc_segmentsP wo); apply /(setU_segment or).
move=> x xs'; move: (s's _ xs'); apply: alse.
move=> x xu; move: (setU_hi xu)=> [y xy ys'].
by move: (s's _ ys') => /Zo_hi;apply.
have sc: forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segmentc r x) s.
move=> x xsr => /Zo_P [] /(inc_segmentsP wo) pa pb.
apply Zo_i;first by apply: segmentc_insetof.
move=> y; rewrite - (segmentc_pr or xsr); case/setU1_P; first apply: pb.
move: (transfinite_unique1 tf tf' pb) => sWx ->.
by move: tf tf'=> [_ _ pf] [_ _ pf']; rewrite (pf _ xsr)(pf' _ xsr) sWx.
move: (transfinite_principle2 wo su sc); move /Zo_P => [_ asW].
move:tf tf'=> [suf sf _][suf' sf' _ ].
apply: function_exten4 => //; [ by rewrite sf sf' | by rewrite sf].
Qed.

Lemma transfinite_aux1 r p s' s'' f' f'':
worder r -> segmentp r s' -> segmentp r s'' -> sub s' s'' ->
transfinite_def (induced_order r s') p f' ->
transfinite_def (induced_order r s'') p f'' ->
f' = restriction1 f'' s'.
Proof.
move=> wo ss' ss'' is'' tf' tf''.
set (f:=restriction1 f'' s').
have or:order r by fprops.
move: tf''=> [[ff'' _] sf'' pb].
have s''s: sub s'' (substrate r) by move: ss''=>[q _]; exact q.
have s's: sub s' (substrate r) by move: ss'=>[q _]; exact q.
have woi: worder (induced_order r s') by apply: induced_wor.
have s'sf'': sub s' (source f'') by rewrite sf''; aw.
have sf: source f = s' by rewrite /f/restriction1; aw.
have suf: surjection f by rewrite /f; apply: restriction1_fs=>//.
have ff: function f by fct_tac.
suff: transfinite_def (induced_order r s') p f.
by apply: (transfinite_unique woi tf').
split => //; aw.
move=> x xs'.
have p1: sub (segment (induced_order r s') x) s' by apply: sub_segment2.
have p2: sub (segment (induced_order r s'') x) (source f'').
by rewrite sf''; apply: sub_segment.
have p3: {inc s', f =1f f''} by move=> a as''; rewrite /f restriction1_V //.
move: (is'' _ xs') => xs''.
have xsi: inc x (substrate (induced_order r s'')) by aw.
have ->: (restriction_to_segment (induced_order r s') x f =
restriction_to_segment (induced_order r s'') x f'').
rewrite -{2} sf in p1.
apply: rts_extensionality =>//; aw.
do 2 rewrite segment_induced_a //.
by move=> a asi; apply: p3; rewrite - sf; apply: p1.
by rewrite - (pb _ xsi); apply: p3.
Qed.

Existence follows from two extension properties

Definition change_target_fun f t := triple (source f) t (graph f).

Lemma transfinite_aux2 r p s tdf: worder r ->
(alls s (segmentp r)) ->
(forall z, inc z s -> transfinite_def (induced_order r z) p (tdf z)) ->
let t := unionf s (fun z => target (tdf z)) in
let f := (common_ext (Lg s id) (fun z => change_target_fun (tdf z) t) t) in
(transfinite_def (induced_order r (union s)) p f /\ target f = t).
Proof.
move=> wo alseg altd.
have or: order r by fprops.
have alfun:forall i, inc i s -> function (tdf i).
move=> i ins; move: (altd _ ins)=> [sf _ _ ]; fct_tac.
have slso:forall i, inc i s -> source (tdf i) = i.
move=> i ins; move: (altd _ ins)=> [_ so _]; move: so; aw.
by move: (alseg _ ins)=> [q _].
simpl.
set si := Lg s id.
set t:= unionf _ _.
pose tde z := change_target_fun (tdf z) t.
have fpe:forall i, inc i s -> function_prop (tde i) (Vg si i) t.
rewrite /si/tde/change_target_fun; bw;move=>i ins;bw.
move: (alfun _ ins)=> fd.
red;aw;split => //.
apply: function_pr; fprops.
apply: (@sub_trans (target (tdf i))); first by apply: f_range_graph.
rewrite /t => x xt; union_tac.
rewrite - f_domain_graph //.
by apply: slso.
have Wfe:forall i a, inc i s-> inc a i -> Vf (tdf i) a = Vf (tde i) a.
move=> i a ins ai; symmetry.
set (x:= Vf (tde i) a ).
have : (inc (J a x) (graph (tde i))).
rewrite /x; move: (fpe _ ins)=> [fu st tg]; apply: Vf_pr3 =>//.
rewrite st /si; bw.
by rewrite /tde /change_target_fun; aw;apply: Vf_pr; apply: alfun.
have agr: (forall i j, inc i s -> inc j s -> sub i j ->
agrees_on (i \cap j) (tde i) (tde j)).
move=> i j ins jns ij.
have ->: (i \cap j = i) by apply/setI2id_Pl.
move: (fpe _ ins)(fpe _ jns)=> [ffi sfi tfi][ffj sfj tfj].
red; rewrite sfi sfj /si; bw; split => //.
move=> a ai /=; rewrite -(Wfe _ _ ins ai) -(Wfe _ _ jns (ij _ ai)).
rewrite (transfinite_aux1 wo (alseg _ ins) (alseg _ jns)
ij (altd _ ins) (altd _ jns)).
rewrite restriction1_V =>//; [ by apply: alfun | by rewrite slso].
have agr':forall i j, inc i s -> inc j s ->
agrees_on ((Vg si i) \cap (Vg si j)) (tde i) (tde j).
move=> i j ins jns; rewrite /si; bw.
case: (segment_dichot_sub wo (alseg _ ins) (alseg _ jns)).
by apply: agr.
rewrite setI2_C.
move=> ji; move: (agr _ _ jns ins ji); rewrite /agrees_on.
by move => [s1 s2 sv]; split => //; move => a ai; symmetry; apply: sv.
have su:sub (union s) (substrate r).
move=> v vu; move: (setU_hi vu)=> [i vi ins].
by move: (alseg _ ins)=> [q _]; apply: q.
have dsi: domain si = s by rewrite /si; bw.
rewrite - dsi in fpe agr'.
have aux:forall x0 x1, inc x0 x1 -> inc x1 s -> sub
(segment (induced_order r (union s)) x0) x1.
move=> x0 x1 x0x1 x1s u us; move: (alseg _ x1s)=> [_ spr].
move: (inc_segment us); rewrite /glt; move => [ux0 nux0].
move: (iorder_gle1 ux0); apply: (spr _ _ x0x1).
move: (extension_covering fpe agr'); set f := (common_ext si tde t).
rewrite dsi;move => [[sf tf gf] _ _ agf].
split=>//.
split.
split => //.
rewrite gf=> y; rewrite /t=> yt; move: (setUf_hi yt)=> [i ins ti].
move: (altd _ ins)=> [sfi sofi vfi].
move:((proj2 sfi) _ ti)=> [z zs Wz].
rewrite (slso _ ins) in zs.
move: (agf _ ins)=> [sis _ prop].
have zf: inc z (source f) by apply: sis; rewrite /si;bw.
ex_tac; rewrite -Wz Wfe //; apply: prop; rewrite /si;bw.
by aw; rewrite tf - setUb_identity.
aw;move=> x xu; move: (setU_hi xu)=> [i xi ins].
have ap: {inc i, f =1f (tdf i)}.
move=> a ai; move: (agf _ ins)=> [sis _ prop]; rewrite Wfe // prop/si; bw.
have p1: (sub i (substrate r)) by move: (alseg _ ins) => [q _]; apply: q.
have p2: (segment (induced_order r i) x = segment r x).
by rewrite segment_induced_a //; apply: alseg.
have ->: (restriction_to_segment (induced_order r (union s)) x f =
restriction_to_segment (induced_order r i) x (tdf i)).
have p3: (segment (induced_order r (union s)) x = segment r x).
rewrite segment_induced_a//; apply: setU_segment =>//.
have p4: sub (segment r x) i.
move: (alseg _ ins) => [_ nsi] y /segmentP [xle _]; apply: (nsi _ _ xi xle).
apply: rts_extensionality =>//; rewrite ? p2 ? p3;
try apply: induced_wor=>//; aw.
rewrite tf/si; move=> u us; move: (p4 _ us)=> ui; apply/setUb_P; bw.
ex_tac; bw.
by apply: alfun.
by rewrite slso.
move=> a asr; apply: (ap _ (p4 _ asr)).
move: (altd _ ins)=> [_ _]; rewrite ap=>//;apply; aw.
Qed.

Lemma transfinite_aux3 r p x g:
worder r -> inc x (substrate r)
-> transfinite_def (induced_order r (segment r x)) p g
-> transfinite_def (induced_order r (segmentc r x)) p
(extension g x (p (restriction_to_segment r x g))).
Proof.
move=> wo xsr tdo.
have or: order r by fprops.
move: (tdo)=> [sug sog Wg].
have ssr: sub (segment r x) (substrate r) by apply: sub_segment.
have sio: substrate (induced_order r (segment r x)) = segment r x by aw.
rewrite sio in sog Wg.
set (tsx:= segmentc r x).
have stsx: (sub tsx (substrate r)) by apply: sub_segmentc.
have sioc: substrate (induced_order r tsx) = tsx by aw.
have nxsg: ~ (inc x (source g)).
by rewrite sog; aw; red; apply: not_in_segment.
set (h:= (restriction_to_segment r x g)).
move: (extension_fs (p h) (proj1 sug) nxsg sug) => sto.
have tos:(segment r x) +s1 x = tsx by rewrite /tsx segmentc_pr//.
red;rewrite sioc; split => //.
rewrite /extension; aw; ue.
move=> y ytsx.
have syx: (sub (segment r y) (segment r x)).
move: ytsx => /segmentcP; apply: segment_monotone =>//.
have fto: function (extension g x (p h)) by fct_tac.
have soto: source (extension g x (p h)) = tsx.
by rewrite/extension; aw; rewrite sog //.
have fg: function g by fct_tac.
have p2: segment (induced_order r tsx) y = segment r y.
apply: segment_induced_a =>//.
rewrite /tsx; apply: segmentc_segment=>//.
case: (equal_or_not y x) => yx.
rewrite yx extension_Vf_out //.
rewrite yx in ytsx p2.
have p1: sub (segment r x) tsx by rewrite -tos; fprops.
apply: f_equal.
apply: rts_extensionality =>//; aw; try ue.
rewrite soto p2; fprops.
red; aw; move=> a asr; rewrite extension_Vf_in //; ue.
have ysx: inc y (segment r x).
by move: ytsx; rewrite -tos; case/setU1_P.
have p1: {inc (segment r x), g =1f (extension g x (p h))}.
move=> u usx /=; rewrite extension_Vf_in //; ue.
have p3: segment (induced_order r (segment r x)) y = segment r y.
by apply: segment_induced_a =>//; apply: segment_segment =>//.
rewrite -p1 // Wg //.
congr (p _).
apply: rts_extensionality =>//; rewrite ? p2 ? p3 ? soto ? sog;
try apply: induced_wor=>//;aw.
apply: (sub_trans syx); rewrite -tos; fprops.
move=> a asr; apply: (p1 _ (syx _ asr)).
Qed.

Definition transfinite_defined r p:= choose (fun f => transfinite_def r p f).

Theorem transfinite_definition r p:
worder r -> exists! f, (transfinite_def r p f).
Proof.
move=> wo; apply /unique_existence.
split; last by move=> x y;apply: (transfinite_unique wo).
set (s:=Zo (segments r) (fun z =>
exists f, transfinite_def (induced_order r z) p f)).
have or: order r by fprops.
have als: forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(inc_segmentsP wo).
have ssu: forall s', sub s' s -> inc (union s') s.
move=> s' s's.
have als': (alls s' (segmentp r)).
by move=> x xs'; apply: (als _ (s's _ xs')).
apply: Zo_i.
apply /(inc_segmentsP wo); apply: setU_segment =>//.
pose tdf z:= transfinite_defined (induced_order r z) p.
have atdf: forall z, inc z s' ->
transfinite_def (induced_order r z) p (tdf z).
move=> z zs'; move: (s's _ zs') => /Zo_P [p1 p2].
apply: (choose_pr p2).
move: (transfinite_aux2 wo als' atdf) => [].
set f:= common_ext _ _ _; move=> p1 p2; by exists f.
have sss: forall x, inc x (substrate r) -> inc (segment r x) s
-> inc (segmentc r x) s.
move=> x xst /Zo_hi [f tdf]; apply: Zo_i.
by apply: segmentc_insetof => //.
exists (extension f x (p (restriction_to_segment r x f))).
apply: (transfinite_aux3 wo xst tdf).
move: (transfinite_principle2 wo ssu sss).
by move /Zo_P; rewrite iorder_substrate //; move=> [_].
Qed.

Lemma transfinite_pr r x p:
worder r -> transfinite_def r p x ->
transfinite_defined r p = x.
Proof.
move=> wo td.
have tdt: (transfinite_def r p (transfinite_defined r p)).
by rewrite /transfinite_defined; apply choose_pr; exists x.
apply: (transfinite_unique wo tdt td).
Qed.

if p sends some functions to E, then the target of function defined by transfinite induction is a subset of E

Theorem transfinite_definition_stable r p F:
worder r ->
(forall f, function f -> segmentp r (source f) -> sub (target f) F ->
inc (p f) F) ->
sub (target (transfinite_defined r p)) F.
Proof.
move=> wo hyp.
set (s:=Zo(segments r) (fun z =>
exists2 f, (transfinite_def (induced_order r z) p f) &(sub (target f) F))).
have or: order r by fprops.
have als: forall x, inc x s -> segmentp r x.
by move=> x /Zo_P [] /(inc_segmentsP wo).
suff: inc (substrate r) s.
move /Zo_P => [p1 [f tdf tfF]].
have aux: (induced_order r (substrate r) =r) by apply: iorder_substrate.
rewrite aux in tdf.
have -> //: (transfinite_defined r p = f) by apply: (transfinite_pr wo tdf).
apply: transfinite_principle2=>//.
move=> s' s's.
have als': (alls s' (segmentp r))
by move=> x xs'; apply: (als _ (s's _ xs')).
apply: Zo_i.
apply/(inc_segmentsP wo); apply: setU_segment =>//.
pose tdf z := transfinite_defined (induced_order r z) p.
have atdf: forall z, inc z s' ->
transfinite_def (induced_order r z) p (tdf z).
move=> z zs'; move: (s's _ zs') => /Zo_P [p1 [f p2 _]].
have aux: (exists f, transfinite_def (induced_order r z) p f).
by exists f.
apply: (choose_pr aux).
move: (transfinite_aux2 wo als' atdf) => [].
set f:= common_ext _ _ _ ; move=> p1 p2; exists f => //.
rewrite p2.
move => u uu; move: (setUf_hi uu)=> [v vs' uv].
move: (s's _ vs') => /Zo_P [vs [g tdg tg]].
move: (atdf _ vs') => tdf1.
have wa: (worder (induced_order r v)).
apply: induced_wor =>//; apply: sub_segment1; apply: (als' _ vs').
rewrite (transfinite_unique wa tdg tdf1) in tg.
by apply: tg.
move=> x xst => /Zo_P [_ [f tdf tfF]]; apply: Zo_i.
by apply: segmentc_insetof.
exists (extension f x (p (restriction_to_segment r x f))).
by apply: (transfinite_aux3 wo xst tdf).
have srx: (sub (segment r x) (substrate r)) by apply: sub_segment.
rewrite /extension; move=> t;aw; case /setU1_P; first by apply: tfF.
move: (tdf)=> [sf sof Wf].
have ff: function f by fct_tac.
have ssf: sub (segment r x) (source f) by rewrite sof; aw; fprops.
move => ->; apply: hyp.
exact (proj1 (restriction1_fs (proj1 sf) ssf)).
rewrite /restriction_to_segment/restriction1; aw.
apply: segment_segment=>//.
rewrite /restriction_to_segment/restriction1; aw.
move=> v /(Vf_image_P ff ssf) [u us ->]; apply: tfF;Wtac.
Qed.

Lemma transfinite_defined_pr r p: worder r ->
transfinite_def r p (transfinite_defined r p).
Proof.
move=> wo; rewrite /transfinite_defined.
move: (transfinite_definition p wo) => /unique_existence [red _].
by apply:choose_pr.
Qed.

Definition ordinal_iso r := transfinite_defined r target.

Lemma transdef_tg1 r (f := ordinal_iso r): worder r ->
forall x, inc x (substrate r) ->
Vf f x = image_by_fun f (segment r x).
Proof.
move => wor x xsr.
move: (transfinite_defined_pr target wor)=> [pa pb pc].
by rewrite (pc _ xsr) corresp_t.
Qed.

Lemma transdef_tg2 r f:
worder r -> surjection f -> source f = substrate r ->
(forall x, inc x (substrate r) -> Vf f x = image_by_fun f (segment r x)) ->
f = ordinal_iso r.
Proof.
move => wor pa pb pc.
have pd: transfinite_def r target f by split => // x /pc ->; rewrite corresp_t.
by move: (transfinite_pr wor pd).
Qed.

Lemma transdef_tg3 r X f:
worder r -> segmentp r X ->
(forall x, inc x X -> f x = fun_image (segment r x) f) ->
forall x, inc x X -> f x = Vf (ordinal_iso r) x.
Proof.
move => wor pa pb.
have srr: sub (substrate r) (substrate r) by fprops.
move: (wor) => [or _].
set A:= fun_image X f.
have ta: forall t, inc t X -> inc (f t) A by move => t tx; apply/funI_P; ex_tac.
set g := Lf f X A.
have sg: surjection g by apply: lf_surjective => // y /funI_P.
have fg: function g by fct_tac.
move => x xX.
have -> : f x = Vf g x by rewrite /g; aw.
have pc := (substrate_segment or).
have pd := (sub_segment1 pa).
have pe: transfinite_def (induced_order r X) target g.
rewrite /g;split; aw => t tX; aw; rewrite corresp_t segment_induced_a //.
have ssg': sub (segment r t) X.
move => s /segmentP [st _]; exact: (proj2 pa _ _ tX st).
have ssg: sub (segment r t) (source g) by rewrite /g; aw.
rewrite (pb _ tX); set_extens w.
move /funI_P => [z za zb]; apply /(Vf_image_P fg ssg); ex_tac.
by rewrite /g; aw; apply: ssg'.
move /(Vf_image_P fg ssg)=> [u us]; rewrite /g; aw; last by apply: ssg'.
move => ->; apply/funI_P; ex_tac.
have pf: transfinite_def (induced_order r (substrate r)) target (ordinal_iso r).
rewrite (iorder_substrate or); exact:(transfinite_defined_pr target wor).
move: (pf) =>[[fs _] ]; rewrite (iorder_sr (proj1 wor) srr) => ss _.
move: (transfinite_aux1 wor pa pc pd pe pf) => ->.
by rewrite restriction1_V // ss.
Qed.

## EIII-2-3 Zermelo's theorem

Given an ordering, let Sx be the segment with endpoint x, considered as an ordered set. Given two orderings, we consider the set of all x with Sx=Sx'. This is a segment, ordered by any of the two induced orders.

Definition common_ordering_set r r' :=
Zo ((substrate r) \cap (substrate r'))
(fun x => segment r x = segment r' x /\
induced_order r (segment r x) = induced_order r' (segment r' x)).

Lemma Zermelo_aux0 r r':
common_ordering_set r r' = common_ordering_set r' r.
Proof.
rewrite /common_ordering_set setI2_C.
set_extens t; move/Zo_P => [pa [pb pc]]; apply: Zo_i => //.
Qed.

Lemma Zermelo_aux1 r r': worder r -> worder r' ->
segmentp r (common_ordering_set r r').
Proof.
rewrite /common_ordering_set=> wor wor'.
split; first by move=> t /Zo_P [] /setI2_P [].
move=> x y.
case: (equal_or_not y x); first by move=> ->.
move => nyx /Zo_P [pa [pb pc]] pd.
have ltyx:glt r y x by split.
have sry: inc y (segment r x) by apply /segmentP.
have sry': inc y (segment r' x) by rewrite - pb.
have syr: inc y (substrate r) by apply: (sub_segment sry).
have syr': inc y (substrate r') by apply: (sub_segment sry').
rewrite /induced_order - pb in pc.
have or: order r by fprops.
have or': order r' by fprops.
apply: Zo_i; first by fprops.
have sryy': (segment r y = segment r' y).
set_extens t; move/segmentP => [ty nty]; apply /segmentP; split=>//;
suff: (inc (J t y) (r \cap (coarse (segment r x)))).
- rewrite pc; move/setI2_P => [] //.
- apply/setI2_i => //; apply/setXp_i => //; apply/segmentP; order_tac.
- move /setI2_P => [] //.
- have aux: glt r' y x by apply/segmentP; rewrite -pb; apply/segmentP.
rewrite pc;apply:setI2_i => //;rewrite pb;apply:setXp_i;apply/segmentP =>//.
order_tac.
split=>//.
rewrite /induced_order - sryy'.
move: (coarse_segment_monotone or pd)=> p1.
set_extens z; move/setI2_P =>[zr zc];
suff: (inc z (r \cap (coarse (segment r x)))).
rewrite pc; move/setI2_P => [] //.
- by move => qa qb; apply: setI2_i => //; apply: p1.
- by apply /setI2_i => //; apply: p1.
- by move /setI2_P => [qa qb]; apply :setI2_i.
- by rewrite pc;apply/setI2_i => //; apply: p1.
Qed.

Lemma Zermelo_aux2 r r' v: worder r -> worder r' ->
v = common_ordering_set r r' -> sub(induced_order r v) (induced_order r' v).
Proof.
rewrite /induced_order /coarse /common_ordering_set.
move=> wor wor' vd.
have or: order r' by fprops.
move=> t /setI2_P [tr] /setX_P [pt Pt Qt].
have pv: J (P t) (Q t) = t by aw.
apply/setI2_P; split; last by apply /setX_P.
move: Qt; rewrite vd => /Zo_P [] /setI2_P [Qtr Qtr'] [ss io].
case: (equal_or_not (P t) (Q t)).
by move=> eq; rewrite -pv eq; order_tac.
move=> neq; rewrite -pv in tr.
have: (inc (P t) (segment r (Q t))) by apply: segment_inc=>//; split.
rewrite ss -{3} pv => aux.
move: (inc_segment aux)=> [h _]; exact h.
Qed.

We prove Zermelo's theorem by considering well-orderings r, and sets S such that the segment Sx with endpoint x is in S, and P(Sx)=x.

Definition Zermelo_axioms E p s r:=
[/\ worder r,
sub (substrate r) E,
(forall x, inc x (substrate r) -> inc (segment r x) s) &
(forall x, inc x (substrate r) -> p (segment r x) = x)].

Lemma Zermelo_aux3 E s p r r':
let q := fun r r' => [/\ sub (substrate r) (substrate r'),
r = induced_order r' (substrate r) & segmentp r' (substrate r)] in
Zermelo_axioms E p s r -> Zermelo_axioms E p s r' ->
q r r' \/ q r' r.
Proof.
move=> q [wor srE alseg pr][wor' srE' alseg' pr'].
move: (Zermelo_aux1 wor' wor)(Zermelo_aux1 wor wor').
rewrite Zermelo_aux0.
set (v:= common_ordering_set r r').
move=> svr' svr.
have io: (induced_order r v = induced_order r' v).
by apply: extensionality; apply: Zermelo_aux2=>//; rewrite Zermelo_aux0.
move: (sub_segment1 svr)(sub_segment1 svr')=> vsr vsr'.
case: (equal_or_not v (substrate r)) => evr.
left; rewrite /q -evr; split => //.
rewrite -io evr;symmetry; apply: iorder_substrate; fprops.
case: (equal_or_not v (substrate r')) => evr'.
right; rewrite /q -evr'; split => //.
rewrite io evr';symmetry; apply: iorder_substrate; fprops.
case: (emptyset_dichot ((substrate r) -s v)) => co.
by case: evr; apply: extensionality=>//; apply: empty_setC.
case: (emptyset_dichot (complement (substrate r') v)) => co'.
by case: evr'; apply: extensionality=>//; apply: empty_setC.
have sc: (sub ((substrate r) -s v) (substrate r)).
by apply: sub_setC.
have sc': (sub ((substrate r') -s v) (substrate r')).
by apply: sub_setC.
move:(worder_total wor) (worder_total wor')=> tor tor'.
move:wor=> [or wo]; move: (wo _ sc co)=> [x []]; aw => /setC_P [xs xc] px.
move:wor'=> [or' wo']; move: (wo' _ sc' co')=> [y []]; aw => /setC_P [ys yc] py.
have p1: (segment r x = v).
set_extens z => zs.
ex_middle aux.
move: (inc_segment zs) => zx.
have zc: inc z ((substrate r) -s v) by apply/setC_P; split=>//; order_tac.
move: (px _ zc) => h.
move: (iorder_gle1 h)=> xz; order_tac.
apply /segmentP.
case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz.
case: xc; move: svr=> [_ h]; apply: (h _ _ zs xz).
have p2: (segment r' y = v).
set_extens z => zs.
ex_middle aux.
move: (inc_segment zs) => zx.
have zc: inc z ((substrate r') -s v) by apply/setC_P; split=>//; order_tac.
move: (py _ zc) => h.
move: (iorder_gle1 h)=> yz; order_tac.
apply /segmentP.
case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz.
case: yc; move: svr'=> [_ h]; apply: (h _ _ zs yz).
have xy: x = y by rewrite - (pr _ xs) -(pr' _ ys) p1 p2.
case: xc.
rewrite /v /common_ordering_set; apply: Zo_i.
apply /setI2_i => //; ue.
rewrite p1 xy p2; split=>//.
Qed.

Lemma Zermelo_aux4 r a (owg := order_with_greatest r a):
worder r -> ~ (inc a (substrate r)) ->
[/\ worder owg, segment owg a = (substrate r) &
forall x, inc x (substrate owg) -> x = a \/
segment owg x = segment r x].
Proof.
move=> wor nas.
move: (order_with_greatest_pr (worder_or wor) nas)=> [[oe se] rv ge].
move: ge=>[asr prop].
split=>//.
set_extens x => xs.
move:(inc_segment xs)=> xa.
have: inc x (substrate owg) by order_tac.
rewrite se => /setU1_P;case =>//.
have ax: x <> a by dneg ax; rewrite -ax.
apply /segmentP; split=>//; apply: prop; rewrite se; fprops.
move=> x; rewrite se => /setU1_P; case; last by left.
move=> xsr; right.
have xsre: inc x (substrate owg) by rewrite se; aw; fprops.
set_extens y; move /segmentP=> [yx nyx]; apply/segmentP; split => //;last first.
by move: yx; rewrite rv; apply: iorder_gle1.
rewrite rv; apply: setI2_i => //;apply /setXp_i => //.
move: (arg1_sr yx); rewrite se => /setU1_P; case => //.
move=> ya; case: nyx.
move: (prop _ xsre); fold owg; rewrite -ya => p1; order_tac.
Qed.

Lemma Zermelo_aux E s p: sub s (powerset E) ->
(forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x))) ->
exists2 r, Zermelo_axioms E p s r & (~ (inc (substrate r) s)).
Proof.
move=> sp pp.
set (m:= Zo (powerset (coarse E)) (fun r => Zermelo_axioms E p s r)).
pose q r r' := [/\ sub (substrate r) (substrate r') ,
r = induced_order r' (substrate r) & segmentp r' (substrate r)].
have qq:(forall r r', inc r m -> inc r' m -> q r r' \/ q r' r).
move=> r r' /Zo_P [rp za] /Zo_P [rp' za'].
apply: (Zermelo_aux3 za za').
set (g:= Lg m id).
have cog: common_worder_axiom g.
rewrite /g / common_worder_axiom/worder_fam;bw;split; fprops.
by red; bw; move=> x xm; bw; move: xm => /Zo_hi [a _].
move=> a b am bm; bw.
move: am bm => /Zo_P [ac za] /Zo_P [bc zb].
by case: (Zermelo_aux3 za zb); move => [_ _]; [right | left ].
red; bw;move=> a b am bm; bw.
move: am bm => /Zo_P [ac za] /Zo_P [bc zb].
case: (Zermelo_aux3 za zb); first by move => [_].
move=> [sba bi siab] sab.
have ssab: (substrate a = substrate b) by apply: extensionality=>//.
have oa: order a by move: za=> [woa _]; fprops.
have ob: order b by move: zb=> [wob _ ]; fprops.
red;rewrite ssab iorder_substrate // bi - ssab iorder_substrate //.
move: (worder_merge cog) => [coex wou alsu ssu ssup].
have dg: domain g = m by rewrite /g; bw.
have Vg: forall a, inc a m -> Vg g a = a by move=> a am; rewrite /g; bw.
move: coex => [om0 som0 pom0].
rewrite dg in alsu ssu ssup som0 pom0.
set (m0:= unionb g) in *.
have Za: (Zermelo_axioms E p s m0).
red; split => //; rewrite som0=> t tu; move: (setUf_hi tu)=> [u ud ts];
move: (ud) => /Zo_P [_ [_ p1 p2 p3]];
move: (ts); rewrite Vg // => tb.
by apply: p1.
by rewrite -(ssu _ _ ud ts); rewrite Vg //; apply: p2.
by rewrite -(ssu _ _ ud ts); rewrite Vg //; apply: p3.
exists m0 => // sm0s.
move:(pp _ sm0s)=> [pE nps].
set (a:= p (substrate m0)) in *.
move: (Zermelo_aux4 wou nps) => [woe seu asu].
move: (order_with_greatest_pr om0 nps) =>[[ou su] up geu].
have Zae: (Zermelo_axioms E p s (order_with_greatest m0 a)).
move: Za=> [p1 p2 p3 p4].
split=>//; rewrite su => t /setU1_P; case.
- apply: p2.
- by move=> ->.
- move=> ts.
have p5: inc t (substrate (order_with_greatest m0 a)) by rewrite su; fprops.
move: (asu _ p5); case.
move=> hyp; rewrite hyp in ts; contradiction.
by move=> ->; apply: p3.
- by move => ->; rewrite seu.
- move=> ts.
have p5: inc t (substrate (order_with_greatest m0 a)) by rewrite su; fprops.
move: (asu _ p5); case.
move=> hyp; rewrite hyp in ts; contradiction.
by move=> ->; apply: p4.
- by move=> ->; rewrite seu.
have um:inc (order_with_greatest m0 a) m.
rewrite /m; apply: Zo_i =>//.
apply /setP_P.
apply: (@sub_trans (coarse (substrate (order_with_greatest m0 a)))).
apply: sub_graph_coarse_substrate; fprops.
have aux: (sub (substrate (order_with_greatest m0 a)) E).
move: Zae=> [_ res _ _]; apply: res.
by apply: setX_Slr.
case: nps.
rewrite som0.
apply: (setUf_i um); rewrite Vg //; rewrite su; fprops.
Qed.

The axiom of choice asserts existence of an element p(x) of E not in x, if x is not E. From this we deduce a well-ordering on E

Theorem Zermelo E: exists r, worder_on r E.
Proof.
set (s:=(powerset E) -s1 E).
have p1: sub s (powerset E) by rewrite /s; apply: sub_setC.
set (p:= fun x => rep (E -s x)).
have p2: forall x, inc x s -> inc (p x) (E -s x).
move=> x xs; rewrite /p; apply: rep_i.
apply: setC_ne.
by move: xs => /setC_P [] /setP_P pa /set1_P xe; split.
have p3: forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x)).
by move => x xs; move: (p2 _ xs) => /setC_P.
move: (Zermelo_aux p1 p3) => [r [xor so alse ps ns]].
exists r; split=> //; ex_middle h; case: ns; apply/setC_P; split.
by apply /setP_P.
by move/set1_P.
Qed.

## EIII-2-4 Inductive sets

Definition inductive r :=
forall X, sub X (substrate r ) -> total_order (induced_order r X) ->
exists x, upper_bound r X x.

Examples of inductive set

Lemma inductive_graphs a b:
inductive (opp_order (extension_order a b)).
Proof.
move: (extension_osr a b)=> [or sr].
move: (opp_osr or) => [ooi osr] X XX.
move: (XX); rewrite osr sr => Xs toX.
have Ha:forall i, inc i X -> function i.
by move=> i iX; move: (Xs _ iX) => /sfun_set_P [].
have Hb:forall i, inc i X -> target i = b.
by move=> i iX; move: (Xs _ iX) => /sfun_set_P [_ ].
move: toX=> [orX]; aw => tor.
set si:= Lg X source.
have Hd: forall i j, inc i (domain si) -> inc j (domain si) ->
agrees_on ((Vg si i) \cap (Vg si j)) i j.
rewrite /si; bw; move=> i j iX jX; bw.
split; first by apply: subsetI2l.
by apply: subsetI2r.
move=> t /setI2_P [ti tj].
case: (tor _ _ iX jX)=> h; move: (iorder_gle1 h)=> h'.
apply: (extension_order_pr h' ti).
symmetry; apply: (extension_order_pr h' tj).
have He:forall i, inc i (domain si) -> function_prop i (Vg si i) b.
rewrite /si; bw; move=> i iX; red; bw;split; fprops.
move: (extension_covering He Hd) => [[fg sg tg] _ _ agg].
set g:= (common_ext si id b).
have gs: (inc g (sub_functions a b)).
apply /sfun_set_P;split => // t tsg.
rewrite sg in tsg; move: (setUf_hi tsg)=> [v].
rewrite {1}/si; bw => vx; rewrite /si; bw => tv.
by move: (Xs _ vx) => /sfun_set_P [_ sv _]; apply: sv.
rewrite /upper_bound osr sr; ex_tac.
move: agg; rewrite /si; bw => agg.
move=> y yX; move: (Xs _ yX)=> ys; move: (agg _ yX)=> ag.
have fy: (function y) by move: ys; fprops.
apply /igraph_pP; apply/extension_order_P1;split => //.
rewrite sub_function //.
move: ag; rewrite /agrees_on; bw;move=> [p1 p2 p3]; split => //.
by move=> u; symmetry; apply: p3.
Qed.

Full and short version of Zorn's lemma

Theorem Zorn_aux r: order r ->
(forall s, sub s (substrate r) -> worder (induced_order r s) ->
(bounded_above r s)) ->
exists a, maximal r a.
Proof.
move=> or zaux.
pose px X v := upper_bound r X v /\ ~ (inc v X).
set (p := fun X => choose (fun v => px X v)).
set (E:= substrate r).
set (s:= Zo (powerset E) (fun X => exists v, px X v)).
have apx: forall X, inc X s -> px X (p X).
by move=> X /Zo_P [_ ev]; apply: choose_pr.
have sp: sub s (powerset E) by rewrite /s; apply: Zo_S.
have zp: forall x, inc x s -> (inc (p x) E /\ ~ (inc (p x) x)).
move=> x xs; move: (apx _ xs); rewrite /px; move=> [up h].
by move: up => [].
move: (Zermelo_aux sp zp)=> [r' [xor so alse ps ns]].
move: (iorder_osr or so) => [oi sr1].
have ext: sub r' (induced_order r (substrate r')).
have gr: sgraph r' by fprops.
move=> x xr.
move: (gr _ xr) => xp; rewrite - xp in xr |- *.
move: (arg2_sr xr) => qs.
move: (arg1_sr xr) => Ps.
case: (equal_or_not (P x) (Q x)) => aux.
rewrite aux; order_tac; aw.
have ltPQ: glt r' (P x) (Q x) by split.
change (gle (induced_order r (substrate r')) (P x) (Q x)); aw.
have Pse: (inc (P x) (segment r' (Q x))) by apply/ segmentP.
move: (alse _ qs)(ps _ qs) => p1 p2; move: (apx _ p1).
rewrite p2; rewrite /px; move=> [[_ h]] _; apply /iorder_gleP => //.
by apply: h.
have r'v: r' = induced_order r (substrate r').
apply: extensionality => //.
move=> t tio.
have p1: order (induced_order r (substrate r')) by fprops.
have p2: sgraph (induced_order r (substrate r')) by fprops.
move: (p2 _ tio) => pt.
rewrite -pt in tio |- *.
have Ps: inc (P t) (substrate r') by move: (arg1_sr tio); aw.
have Qs: inc (Q t) (substrate r') by move: (arg2_sr tio); aw.
case: (total_order_pr2 (worder_total xor) Qs Ps) =>//.
move=> [lePQ nPQ]; move: (ext _ lePQ)=>tio'; case: nPQ; order_tac.
rewrite r'v in xor.
move: (zaux _ so xor) => [u [us ub]].
exists u.
split =>//; move=> x ux.
case: (equal_or_not u x) => h; first by [].
have xu: (glt r u x) by split.
case: ns; apply: Zo_i; [ by apply/setP_P | exists x; split].
split; first by order_tac.
move=> y ys'; move: (ub _ ys')=> yu; order_tac.
move=> xs'; move: (ub _ xs')=> xu'; order_tac.
Qed.

Theorem Zorn_lemma r: order r -> inductive r ->
exists a, maximal r a.
Proof.
move=> or isr; apply: Zorn_aux =>//.
by move=> s ssr wo; red; apply: isr =>//; apply: worder_total.
Qed.

Consequences

Lemma inductive_max_greater r a: order r -> inductive r ->
inc a (substrate r) -> exists2 m, maximal r m & gle r a m.
Proof.
move=> or isr asr.
set (F:= Zo (substrate r)(fun z => gle r a z)).
have Fs: sub F (substrate r) by rewrite /F; apply: Zo_S.
move: (iorder_osr or Fs) => [oi sr].
have aF: inc a F by rewrite /F; apply: Zo_i=> //; order_tac.
have isF: inductive (induced_order r F).
move=> u; aw=> uF; rewrite iorder_trans // => toi.
have tos: (sub (u +s1 a) (substrate r)).
apply: sub_trans Fs.
by move=> t; case /setU1_P ; [ apply: uF| move=> ->].
move: (iorder_osr or tos) => [oit sit].
have toit: total_order (induced_order r (u +s1 a)).
split=>//; rewrite sit.
have susr: sub u (substrate r) by apply: sub_trans Fs.
move=> x y ; case /setU1_P=> hx; case /setU1_P => hy.
- move: toi => [_]; aw => h.
move: (h _ _ hx hy); case => xx; [left | right];
apply/iorder_gleP; fprops; apply (iorder_gle1 xx).
- rewrite hy;right; apply/iorder_gleP; fprops.
by move: (uF _ hx); move /Zo_P => [].
- rewrite hx;left; apply/iorder_gleP; fprops.
by move: (uF _ hy); move /Zo_P => [].
- rewrite hx hy; left;apply/iorder_gleP; fprops.
by move: aF; move /Zo_P => [].
move: (isr _ tos toit) => [b [bs bub]].
move: (bub _ (setU1_1 a u)) => ab.
idtac.
have bF: inc b F by rewrite /F; apply: Zo_i.
exists b; split; aw=>//.
move=> y yu.
by move: (bub _ (setU1_r a yu)) => yb; apply/iorder_gleP => //; apply: uF.
move:(Zorn_lemma oi isF)=> [b []]; aw => bF bm.
move: (bF) => /Zo_P [bs ab].
exists b => //.
split =>// x h; apply: bm; apply/iorder_gleP => //; apply: Zo_i; order_tac.
Qed.

Lemma inductive_powerset A F: sub A (powerset F) ->
(forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) ->
sub S A ->inc (union S) A) ->
inductive (sub_order A).
Proof.
move=> sp Sp X XA [oX tX].
move: (sub_osr A) => [or1 sr1].
rewrite iorder_sr in tX; fprops; rewrite sr1 in XA.
exists (union X).
have p1: inc (union X) A.
apply: Sp =>//;move=> x y xX yX.
move: (tX _ _ xX yX); case.
by move /(iorder_gleP _ xX yX) => /sub_gleP [_ _ h]; left.
by move /(iorder_gleP _ yX xX) => /sub_gleP [_ _ h]; right.
split; first by ue.
by move=> y yX; apply /sub_gleP;split => //;fprops; apply: setU_s1.
Qed.

Lemma maximal_in_powerset A F: sub A (powerset F) ->
(forall So, (forall x y, inc x So -> inc y So -> sub x y \/ sub y x) ->
sub So A -> inc (union So) A) ->
exists a, maximal (sub_order A) a.
Proof.
move=> Ap /(inductive_powerset Ap).
by move: (sub_osr A) => [oA sr1];apply: Zorn_lemma.
Qed.

Lemma minimal_in_powerset A F: sub A (powerset F) -> nonempty A ->
(forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) ->
sub S A -> nonempty S -> inc (intersection S) A) ->
exists a, minimal (sub_order A) a.
Proof.
move=> Ap [x xA] pA.
move: (sub_osr A) => [oA sr1].
move: (opp_osr oA) => [ooA soA].
have ioA: inductive (opp_order (sub_order A)).
move => X; rewrite soA sr1 => XA;rewrite /total_order.
rewrite iorder_sr // ? soA ? sr1 //.
move=> [pb pc]; rewrite /upper_bound soA sr1.
case: (emptyset_dichot X) => neX.
exists x; rewrite neX;split => // y; case; case.
have iXA:inc (intersection X) A.
apply: pA =>//; move=> a b aX bX;
by move: (pc _ _ aX bX); case => h; move: (iorder_gle1 h) =>
/igraph_pP /sub_gleP [_ _]; [right | left].
exists (intersection X); split; first by aw; ue.
move=> y yX;apply /igraph_pP; apply /sub_gleP;split; fprops.
by apply: setI_s1.
move: (Zorn_lemma ooA ioA)=> [a ] /(maximal_opp oA).
by exists a.
Qed.

## EIII-2-5 Isomorphisms of well-ordered sets

Uniqueness of morphism between segments of well-ordered sets

Lemma increasing_function_segments r r' f g:
worder r -> worder r' ->
increasing_fun f r r' -> strict_increasing_fun g r r'->
segmentp r' (range (graph f)) ->
forall x, inc x (source f) -> gle r' (Vf f x) (Vf g x).
Proof.
move=> wor wor'
[or or' [ff sf tf] incf] [_ _ [fg sg tg] sing] sr x xsf.
set (s :=Zo (source f) (fun x => (glt r' (Vf g x) (Vf f x)))).
have sfsg: source f = source g by ue.
move: (worder_total wor) => tor.
move: (worder_total wor') => tor'.
have Wfsr': inc (Vf f x) (substrate r') by rewrite - tf; fprops.
have Wgsr': inc (Vf g x) (substrate r').
by rewrite sfsg in xsf;rewrite - tg; fprops.
case: (total_order_pr2 tor' Wgsr' Wfsr') =>// Wlt.
have nes: nonempty s by exists x; rewrite /s; apply: Zo_i.
have ssf: sub s (source f) by rewrite /s; apply: Zo_S.
rewrite sf in ssf; move: wor=> [_ pwor].
move:(pwor _ ssf nes)=> [y []]; aw => ys yle.
move: ys => /Zo_P [ysf [leWy neWy]].
have Wrg: inc (Vf f y) (range (graph f)) by Wtac.
move: sr => [ _ sr']; move: (sr' _ _ Wrg leWy).
move/(range_fP ff) => [z zf vv].
have lt1: glt r' (Vf f z) (Vf f y) by rewrite - vv; split =>//.
have lt2: glt r z y.
have lt3: (glt r z y \/ gle r y z).
rewrite sf in ysf zf; apply: (total_order_pr2 tor zf ysf).
case: lt3=>// yz; move: (incf _ _ yz)=> lt4; order_tac.
have Wzf: inc (Vf f z) (substrate r') by rewrite - tf; fprops.
have Wzg: inc (Vf g z) (substrate r')
by rewrite sfsg in zf;rewrite- tg; fprops.
case: (total_order_pr2 tor' Wzg Wzf) => h.
have zs: (inc z s) by rewrite /s; apply: Zo_i.
move: (yle _ zs)=> yz; move: (iorder_gle1 yz) => lt3.
order_tac.
move: (sing _ _ lt2); rewrite vv => lt3; order_tac.
Qed.

Lemma isomorphism_worder_unique r r' x y:
worder r -> worder r' -> segmentp r' (range (graph x)) ->
segmentp r' (range (graph y)) ->
order_morphism x r r' -> order_morphism y r r'
-> x = y.
Proof.
move=> wor wor' srx sry mx my.
move:(order_morphism_increasing mx) => six.
move:(order_morphism_increasing my) => siy.
move: (strict_increasing_w six)=> sx.
move: (strict_increasing_w siy)=> sy.
move: mx my=> [_ or' [fx srcx tx] _][_ _ [fy srcy ty] _].
apply: function_exten =>//; try ue.
move=> a asx.
move: (increasing_function_segments wor wor' sx siy srx asx) => p1.
rewrite srcx - srcy in asx.
move: (increasing_function_segments wor wor' sy six sry asx) => p2.
order_tac.
Qed.

Theorem isomorphism_worder r r': worder r -> worder r' ->
let iso:= (fun u v f =>
segmentp v (range (graph f)) /\ order_morphism f u v) in
(exists! f,iso r r' f) \/ (exists! f, iso r' r f).
Proof.
move=> wor wor' iso.
set (E:= substrate r).
set (E':= substrate r').
have or: order r by fprops.
have or': order r' by fprops.
move: (extension_osr E E').
set o1:= (extension_order E E'); set o2:= opp_order o1.
move => [oe soe1]; move: (opp_osr oe) => [ooe osr].
have soe: sub_functions E E' = substrate o2 by ue.
set (s:= (Zo (sub_functions E E') (fun z => exists2 u,
segmentp r u & iso (induced_order r u) r' z))).
have ssee: sub s (sub_functions E E') by rewrite /s; apply: Zo_S.
have sse: sub s (substrate o1) by ue.
have ssoxee: sub s (substrate o2) by ue.
have ins:inductive (induced_order o2 s).
move=> X;rewrite (iorder_sr ooe ssoxee) => Xs;rewrite(iorder_trans _ Xs)=> pX.
have Xse:sub X (sub_functions E E') by apply: (sub_trans Xs ssee).
have Xsoe:sub X (substrate o2) by ue.
have alseg: forall x, inc x s -> segmentp r (source x).
move=> x /Zo_hi [u ru [_ bb]]. move: bb => [_ _ [_ -> _] _].
by aw;apply: sub_segment1.
have alsegr: forall x, inc x s -> segmentp r' (range (graph x)).
by move=> x /Zo_hi [u _ [sv _]].
have Xso: sub X (substrate o1) by ue.
move: pX => [_ ]; aw => ppX.
have cov: forall u v x, inc u X -> inc v X -> inc x (source u) ->
inc x (source v) -> Vf u x = Vf v x.
move=> u v x uX vX xsu xsv.
move: (ppX _ _ uX vX); case => h; move: (iorder_gle1 h);
move/igraph_pP/ extension_orderP => [_ _ h0];
[ | symmetry];apply: extends_sV => //.
move:(sup_extension_order2 Xse cov)=> [x [lubx sx rgx gx]].
move: lubx => /(lubP ooe Xsoe) [[xsoe xb] lub]; rewrite - soe in xsoe.
have xs: inc x s.
have ssx: segmentp r (source x).
rewrite sx; apply: setUf_segment =>//.
red;by bw;move=> a aX; bw;apply: alseg; apply: Xs.
rewrite /s; apply: Zo_i=>//; exists (source x) => //.
have srgx: segmentp r' (range (graph x)).
rewrite rgx; apply: setUf_segment =>//.
by red;bw;move=> a aX; bw;apply: alsegr; apply: Xs.
have sxsr: sub (source x) (substrate r) by move: ssx=> [].
have srxs: sub (range (graph x)) (substrate r') by move: srgx => [].
have xi: (forall a b,
inc a (source x) -> inc b (source x) ->
(gle (induced_order r (source x)) a b <->
gle r' (Vf x a) (Vf x b))).
move=> a b; rewrite sx => asX bsX.
apply: (iff_trans(iorder_gleP r asX bsX)).
move: (setUf_hi asX)=> [u uX].
move: (setUf_hi bsX)=> [v vX].
rewrite Lg_domain in uX vX; bw => bv au.
have [w [wX asw bsw]] :exists z,
[/\ inc z X, inc a (source z) & inc b (source z)].
move: (ppX _ _ uX vX) ; case => h; move: (iorder_gle1 h);
move/igraph_pP/ extension_orderP => [_ _ ext];
move: (extends_Ssource ext)=> sext.
by move: (sext _ au) => ax; exists v.
by move: (sext _ bv) => ax; exists u.
rewrite - (extension_order_pr (xb _ wX) asw).
rewrite - (extension_order_pr (xb _ wX) bsw).
move:(Xs _ wX) => /Zo_hi [z [sz _ [_ [_ _ [_ sf _] ifz]]]].
rewrite (iorder_sr or sz) in sf; rewrite - sf in ifz.
split; last by move /(ifz _ _ asw bsw);apply:iorder_gle1.
move => lab; apply /(ifz _ _ asw bsw);apply/(iorder_gleP ) => //.
move: xsoe => /sfun_set_P [fx srcx tx].
move: (iorder_osr or srcx) => [pa pb].
split => //.
exists x.
split; first by rewrite iorder_sr //.
move=> y yX; move: (Xs _ yX)=> ys.
by apply /iorder_gleP => //; apply: xb.
move:(iorder_osr ooe ssoxee) => [oio sio].
move: (Zorn_lemma oio ins) => [f []]; aw =>fis fmax.
move: (fis) => /Zo_P [fee [x sx xiso]].
case: (equal_or_not x (substrate r)) => h.
move: xiso; rewrite h iorder_substrate //; move=> xiso.
left; apply /unique_existence;split; first by exists f.
move=> a b [s1 m1][s2 m2].
by apply: (isomorphism_worder_unique (r:=r) (r':=r')).
right; apply /unique_existence;split; last first.
move=> a b [s1 m1][s2 m2].
by apply: (isomorphism_worder_unique (r:=r') (r':=r)) =>//.
case: (equal_or_not (range (graph f)) (substrate r'))=> h'.
move: xiso => [_ xiso]; move: (order_morphism_fi xiso) => injf.
set (g:= triple E' E (inverse_graph (graph f))).
move: xiso=> [_ _ [ff sf tf] vf].
have gf: sgraph (graph f) by fprops.
have sf': source f = x by rewrite sf; aw; apply: sub_segment1.
have rgg: range (graph g) = x by rewrite /g; aw; rewrite igraph_range; aw.
have fg: function g.
rewrite /g; apply: function_pr.
split;fprops; move=> a b /=.
move/igraphP=> [pa J1g] /igraphP [pb J2g] sv.
rewrite - sv in J2g; move: (injective_pr3 injf J1g J2g).
by apply: pair_exten.
by move: rgg; rewrite /g; aw; move=> ->;move: sx=> [xe _].
rewrite igraph_domain =>//.
exists g.
red; rewrite rgg; rewrite /order_morphism;split => //.
split => //; first by split => //;try solve [ rewrite /g; aw].
move=> a b asg bsg.
have fgp: (forall u, inc u (source g) ->
(inc (Vf g u) (source f) /\ Vf f (Vf g u) = u)).
move=> u usg; move: (Vf_pr3 fg usg); rewrite {2} /g; aw.
move/igraph_pP => Jg; split; [ Wtac | symmetry;apply: (Vf_pr ff Jg)].
move: (fgp _ asg)(fgp _ bsg)=> [W1s va][W2s vb].
rewrite -{1} va -{1} vb.
rewrite - (vf _ _ W1s W2s); split; first (by apply:iorder_gle1).
move => lab; apply/iorder_gleP => //; ue.
case: (well_ordered_segment wor sx)=> aux; first by contradiction.
move: aux=> [a asr xa].
move: xiso=> [st [_ _ [ff sf tf] isf]].
case: (well_ordered_segment wor' st)=> aux; first by contradiction.
move: aux=> [b vsr tb].
set (g:=extension f a b).
have sfx: source f = x by rewrite sf; aw;rewrite xa; apply: sub_segment.
have asf: ~ (inc a (source f)) by rewrite sfx xa; move;apply: not_in_segment.
have fg:function g by rewrite /g; apply: extension_f.
have tg: target g = E'.
rewrite/g /extension; aw; rewrite tf /E'; by apply: setU1_eq.
have sg: source g = segmentc r a.
by rewrite /g/extension; aw; rewrite sfx xa; apply: segmentc_pr.
have sap: forall a, sub (segmentc r a) (substrate r).
move=> t; rewrite/segmentc/interval_uc; apply: Zo_S.
have rgg: (range (graph g) = segmentc r' b).
rewrite/g/extension; aw; rewrite - segmentc_pr // range_setU1; ue.
have gs: inc g s.
rewrite /s; apply: Zo_i.
by apply/sfun_set_P;split => //; rewrite sg; apply: sap.
exists (segmentc r a).
by apply: segmentc_segment.
split; first by rewrite rgg; apply: segmentc_segment.
move: (iorder_osr or (sap a)) => []; rewrite - sg => pa pb.
red;split => //; move=> u v; rewrite sg; rewrite - segmentc_pr //.
move => qa qb; apply: (iff_trans (iorder_gleP r qa qb)).
move: qa qb; rewrite - xa - sfx => /setU1_P ut /setU1_P vt.
have p1: forall w, inc w (source f) -> glt r' (Vf f w) b.
move=> w wsf.
have: inc (Vf f w) (range (graph f)) by Wtac.
by rewrite tb; move/segmentP.
have p2: forall w, inc w (source f) -> glt r w a.
by move=> w; rewrite sfx xa; move/segmentP.
case: ut => hu; [rewrite extension_Vf_in // | rewrite hu extension_Vf_out //].
case:vt => hv;[rewrite extension_Vf_in // | rewrite hv extension_Vf_out //].
rewrite - isf //.
rewrite - sfx; symmetry;apply /(iorder_gleP r hu hv).
move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _]; by split.
case:vt => hv; [rewrite extension_Vf_in // | rewrite hv extension_Vf_out //].
move: (p1 _ hv)(p2 _ hv)=> [e1 ne1][e2 ne2].
split => h'';[ case: ne2 | case: ne1];order_tac.
by split => _; order_tac.
have eqfg: g = f.
have pa: inc g (sub_functions E E') by rewrite /g/extension; fprops.
have pb: sub (graph f) (graph g) by rewrite corresp_g;fprops.
have pc: sub (target f) (target g) by rewrite corresp_t ; fprops.
apply: fmax; apply /iorder_gleP => //; apply /igraph_pP.
apply /extension_orderP;split => //.
case: asf; rewrite -eqfg sg.
by apply: inc_bound_segmentc.
Qed.

Consequences

Lemma unique_isomorphism_onto_segment r f: worder r ->
segmentp r (range (graph f)) -> order_morphism f r r ->
f = identity (substrate r).
Proof.
move=> wor seg mor.
have [pa pb]: segmentp r (range (graph (identity (substrate r)))) /\
order_morphism (identity (substrate r)) r r.
split.
have [_ si]:(bijection (identity (substrate r))) by apply: identity_fb.
rewrite (surjective_pr3 si); aw; apply: substrate_segment; fprops.
apply: identity_morphism; fprops.
by case: (isomorphism_worder wor wor); move /unique_existence=> [_]; apply.
Qed.

Lemma bij_pair_isomorphism_onto_segment r r' f f':
worder r -> worder r' ->
segmentp r' (range (graph f)) -> order_morphism f r r' ->
segmentp r (range (graph f')) -> order_morphism f' r' r ->
(order_isomorphism f r r' /\ order_isomorphism f' r' r /\
f = inverse_fun f').
Proof.
move=> wor wor' sr1 om sr2 om'.
move: (om)(om')=>[or or' [ff sf tf] fp] [_ _ [ff' sf' tf'] fp'].
have gf: sgraph (graph f) by fprops.
have gf': sgraph (graph f') by fprops.
have cff': (f \coP f') by red; split => //; ue.
have cf'f: (f' \coP f) by red; split => //; ue.
move: (compose_order_morphism om' om) => mor1.
move: (compose_order_morphism om om') => mor2.
have fc: function (f' \co f) by fct_tac.
have srg: segmentp r (range (graph (f'\co f))).
split.
have <-: target (f' \co f) = substrate r by aw.
by apply: f_range_graph.
move=> x y.
rewrite /compose; aw; rewrite (compg_range _ gf).
move/dirim_P=> [u urg p2].
have xrg: (inc x (range (graph f'))) by ex_tac.
have usr: inc u (source f') by Wtac.
move => yx; move:sr2 => [_ sr2]; move: (sr2 _ _ xrg yx).
move /(range_fP ff') => [v vsf' vp].
move: yx; rewrite (Vf_pr ff' p2) vp -fp'// => yr.
move:sr1 => [_ sr1]; move: (sr1 _ _ urg yr) => va.
apply /dirim_P; ex_tac; Wtac.
have srg': segmentp r' (range (graph (compose f f'))).
have fc': function (f \co f') by fct_tac.
split.
have <-: target (f \co f') = substrate r' by aw.
by apply: f_range_graph.
move => x y.
rewrite /compose; aw; rewrite (compg_range _ gf').
move/dirim_P=> [u urg p2].
have xrg: (inc x (range (graph f))) by ex_tac.
have usr: inc u (source f) by Wtac.
move => yx; move:sr1 => [_ sr1]; move: (sr1 _ _ xrg yx).
move /(range_fP ff) => [v vsf' vp].
move: yx; rewrite (Vf_pr ff p2) vp -fp// => yr.
move:sr2 => [_ sr2]; move: (sr2 _ _ urg yr) => va.
apply /dirim_P; ex_tac; Wtac.
move: (unique_isomorphism_onto_segment wor srg mor2) => p1.
move: (unique_isomorphism_onto_segment wor' srg' mor1) => p2.
rewrite - sf in p1; rewrite - sf' in p2.
move: (bijective_from_compose cff' cf'f p2 p1) => [p3 p4 p5].
rewrite /order_isomorphism.
split => //.
Qed.

Lemma isomorphic_subset_segment r a:
worder r -> sub a (substrate r) ->
exists w, exists f, segmentp r w /\
order_isomorphism f (induced_order r a) (induced_order r w).
Proof.
move=> wo asr.
move: (induced_wor wo asr) => woi.
move: (isomorphism_worder woi wo).
case; move/unique_existence=> [[f [sr h]] _];
move: (order_morphism_fi h) => [ff injf];
move: h => [oir or [_ sf tf] fp].
move: sf; aw => sf.
have ta: lf_axiom (Vf f) (source f) (range (graph f)).
by move=> c csf /=; Wtac.
set (g := Lf (Vf f) (source f) (range (graph f))).
exists (range (graph f)); exists g.
have aux:sub (range (graph f)) (substrate r) by move:sr => [].
have gf: sgraph (graph f) by fprops.
rewrite /order_isomorphism /g;split => //; split => //.
apply: (proj1 (iorder_osr or aux)).
split; aw;fprops;apply: lf_bijective =>//.
move=> y /(range_fP ff) [x pa pb]; ex_tac.
red; aw;move=> x y xsf ysf; aw;apply: (iff_trans (fp _ _ xsf ysf)).
split; [ move => aux1; apply/iorder_gleP => //; Wtac | apply: iorder_gle1].
case: (well_ordered_segment woi sr)=> hyp.
rewrite -hyp in tf.
have oi: order_isomorphism f r (induced_order r a).
red; split => //; split => //;last by rewrite -hyp tf.
split=>//; apply: surjective_pr4 =>//.
move: (inverse_order_is oi) => ioi.
exists (substrate r); exists (inverse_fun f).
split; first by apply: substrate_segment.
rewrite iorder_substrate //.
move: hyp=>[x xsr rgf].
move: xsr; aw => xsr.
have xsf: inc x (source f) by rewrite sf; apply: asr.
have Ws: inc (Vf f x) (segment (induced_order r a) x).
by rewrite -rgf; Wtac.
set (s :=Zo (source f) (fun a => (glt r (Vf f a) a))).
have nes: nonempty s.
exists x; apply: Zo_i => //.
move: (inc_segment Ws); apply: (iorder_gle2).
have ssf: sub s (substrate r) by rewrite - sf /s;apply: Zo_S.
move: wo=> [_ wor].
move: (wor _ ssf nes) => [y []]; aw => ys ley.
move: ys => /Zo_P [ysf [leW neW]].
have p1: inc (Vf f y) (source f) by rewrite sf; order_tac.
have p2: inc (Vf f y) s.
apply: Zo_i =>//; split; last by dneg h; apply: injf.
move: leW;rewrite (fp _ _ p1 ysf) => leW; apply: (iorder_gle1 leW).
move: (iorder_gle1 (ley _ p2)) => geW.
case: neW; order_tac.
Qed.

Two isomorphic segments of a well-ordered set are equal

Lemma segments_iso1 r A B: worder r -> sub A B ->
segmentp r A -> segmentp r B ->
(induced_order r B) \Is (induced_order r A) -> A = B.
Proof.
move => woa AB sA sB oi.
move: oi => [f [ora orb [ [[ff injf] sjf] sf tf] isf]].
have oa: order r by move: woa => [o _].
have As: sub A (substrate r) by apply: sub_segment1.
have Bs: sub B (substrate r) by apply: sub_segment1.
move: sf tf; aw=> sf tf.
rewrite - sf in injf isf.
have ta: lf_axiom (Vf f) B B.
move=> t tx; apply: AB; rewrite - tf; Wtac; ue.
set g := Lf (Vf f) B B.
have fg: function g by apply: lf_function.
have rg: (range (graph g) = A).
rewrite - tf;set_extens t.
move /(range_fP fg)=> [u];rewrite /g lf_source => uc; aw => ->; Wtac; ue.
move=> tif; move: ((proj2 sjf) _ tif) => [u usf].
rewrite sf in usf;move=> <-; apply /(range_fP fg).
exists u; rewrite /g; aw; split => //.
have sr: segmentp (induced_order r B) (range (graph g)).
rewrite rg; red; aw;split => //.
move => x y xA leyx; move: (iorder_gle1 leyx).
move: sA xA; rewrite /segmentp; move=>[_]; apply.
have om: order_morphism g (induced_order r B)(induced_order r B).
red; split => //; rewrite /g; aw.
split; aw.
red; aw; move=> x y xB yB /=; aw.
move:(iorder_gleP r (ta _ xB) (ta _ yB)) => xx.
red in isf; rewrite sf in isf.
apply: (iff_trans (isf _ _ xB yB)).
rewrite - sf in xB yB.
move: (Vf_target ff xB) (Vf_target ff yB); rewrite tf.
move => f1a f2a.
apply: (iff_trans (iorder_gleP r f1a f2a)).
by symmetry.
move: (induced_wor woa Bs) => wob.
move: (unique_isomorphism_onto_segment wob sr om) => gi.
symmetry;move: rg; rewrite gi; aw; rewrite surjective_pr3 //; aw.
by move: (identity_fb B) => [_ ok].
Qed.

Lemma segments_iso2 a A B: worder a ->
inc A (segments a) -> inc B (segments a) ->
(induced_order a A) \Is (induced_order a B) -> A = B.
Proof.
move=> woa As Bs.
move: (worder_total (segments_worder woa)) => [or].
rewrite (proj2 (sub_osr _)) => tor; move: (tor _ _ As Bs).
move: As Bs;move/(inc_segmentsP woa)=> As /(inc_segmentsP woa) Bs.
case; move /sub_gleP=> [_ _ sAB] oi.
move: (orderIS oi) => oi'; apply: (segments_iso1 woa)=>//.
symmetry; apply: (segments_iso1 woa)=>//.
Qed.

We rewrite isomorphism_worder: two well-ordered sets is isomorphic, or one is isomorphic to a segment of the other

Lemma isomorphism_worder2 r r': worder r -> worder r' ->
[\/ r \Is r',
(exists2 x, inc x (substrate r) & (induced_order r (segment r x)) \Is r') |
(exists2 x, inc x (substrate r') & (induced_order r' (segment r' x)) \Is r)].
Proof.
move => wor wor'.
case: (isomorphism_worder wor wor'); move /unique_existence=> [[f [fp1 fp2]] _];
move: (order_morphism_fi fp2) => injf;
move: fp2 => [pa pb [pc pd pe] pf].
case : (well_ordered_segment wor' fp1) => eq1.
constructor 1;exists f; red; split => //; split => //.
split =>//; apply: surjective_pr4 => //;apply: extensionality.
fct_tac.
rewrite eq1 pe; fprops.
move: eq1 => [x xsr' rgx].
constructor 3; ex_tac; apply: orderIS.
move: (@sub_segment r' x) => p1.
move: (iorder_osr pb p1) => [qa qb].
exists (restriction1 f (source f)); split => //.
red; rewrite qb /restriction1; aw; split => //.
by apply: restriction1_fb.
by rewrite -rgx - image_by_fun_source.
red; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V pc ssf ax) (restriction1_V pc ssf bx); split.
move/(pf _ _ ax bx) => e1; apply/iorder_gleP =>//; rewrite -rgx; Wtac.
by move/iorder_gle1 => /(pf _ _ ax bx).
case : (well_ordered_segment wor fp1) => eq1.
constructor 1;apply: orderIS; exists f; red; split => //.
split => //;split =>//; apply: surjective_pr4 => //;apply: extensionality.
fct_tac.
rewrite eq1 pe; fprops.
move: eq1 => [x xsr rgx].
constructor 2;ex_tac; apply: orderIS.
move: (@sub_segment r x) => p1.
move: (iorder_osr pb p1) => [qa qb].
exists (restriction1 f (source f)); red; split => //.
rewrite qb /restriction1; split; aw; first by apply: restriction1_fb => //.
by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
red; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V pc ssf ax) (restriction1_V pc ssf bx); split.
move/(pf _ _ ax bx) => e1; apply/iorder_gleP =>//; rewrite -rgx; Wtac.
by move/iorder_gle1 => /(pf _ _ ax bx).
Qed.

## EIII-2-6 Lexicographic Products

Given a family of orders g and an ordering r on the index, we compare two elements x and x' of the product by comparing x(i) and x'(i) where i is the least index where the quantities differ

Definition order_prod_r r g :=
fun x x' =>
forall j, least (induced_order r (Zo (domain g)
(fun i => Vg x i <> Vg x' i))) j -> glt (Vg g j) (Vg x j)(Vg x' j).

Definition orprod_ax r g:=
[/\ worder r, substrate r = domain g & order_fam g].

Definition order_prod r g :=
graph_on (order_prod_r r g)(prod_of_substrates g).

Lemma orprod_osr r g:
orprod_ax r g -> order_on (order_prod r g) (prod_of_substrates g).
Proof.
move=> [wor sr ao].
have aux: forall x, order_prod_r r g x x.
move=> x j [js _]; move: js; aw; fprops; last by rewrite sr; apply: Zo_S.
by move /Zo_hi; case.
have osr: substrate (order_prod r g) = prod_of_substrates g.
rewrite /order_prod graph_on_sr //.
split => //.
have tor: total_order r by apply: worder_total.
move:wor=> [or wor].
rewrite/order_prod.
apply: order_from_rel1; last by move=> u up; apply: aux.
rewrite /order_prod_r - sr => y x z xy yz j [].
aw; try apply: Zo_S.
move /Zo_P => [jd jxy] jp.
set (s:= Zo (substrate r) (fun i => [\/ Vg x