(** * Theory of Sets EIII-2 Well ordered sets 
Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm).  *)

(* $Id: sset6.v,v 1.80 2016/05/18 14:54:53 grimm Exp $ *)


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 ->
    has_least (induced_order r x). 

Definition worder_r (r: relation) :=
  order_r r /\ forall x, {inc x, reflexive_r r} -> nonempty x ->
    has_least (graph_on r x). 

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 -> {inc x, reflexive_r r}  ->  
  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 => s sx nes.
have rs: {inc s, reflexive_r r} 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.
rewrite (iorder_sr gor ss) => y ys; aw.
move: (lea _ ys) => /graph_on_P1 [pa pb pc]; apply/iorder_gleP => //.
by apply/graph_on_P1;split => //; apply: sx.
Qed.

Lemma worder_prop r x: worder r -> sub x (substrate r) -> nonempty x ->
  exists2 a, inc a x & (forall b, inc b x -> gle r a b).
Proof.
move => [or wor] xsr nex; move:(wor _ xsr nex) => [a []]; aw.
by move=> ax ap; ex_tac => b /ap /iorder_gle1.
Qed.

Lemma worder_prop_rev r: order r ->
  (forall x, sub x (substrate r) -> nonempty x ->
    exists2 a, inc a x & (forall b, inc b x -> gle r a b)) ->
  worder r.
Proof.
move => h1 h2; split => // x xsr nex; move: (h2 x xsr nex) => [a ax ap].
by exists a; split; aw => b bx; apply/iorder_gleP => //; apply: ap.
Qed.
  
Lemma worder_invariance r r':
  r \Is r' -> worder r -> worder r'.
Proof. 
move=> [f [or or' [bf sf tf] sif]] wor.
apply:(worder_prop_rev or') =>// x xsr [y yx].
set A := Vfs (inverse_fun f) x. 
have bif := (inverse_bij_fb bf).
have fi: function (inverse_fun f) by fct_tac.
have sxt: (sub x (target f)) by rewrite tf.
have sxs: (sub x (source (inverse_fun f))) by aw. 
have sx :source f = (target (inverse_fun f)) by aw.
have Asx: sub A (substrate r). 
   rewrite - sf sx; apply: sub_trans (fun_image_Starget fi).
   by apply: dirim_S.
have neA: (nonempty A).  
  exists (Vf (inverse_fun f) y); apply /(Vf_image_P fi sxs); ex_tac.
move: (worder_prop  wor Asx neA) => [z zA zle].
move: (zA) => /(Vf_image_P fi sxs) [u ux Wu].
ex_tac; move =>// v vx. 
have utx: inc u (target f) by apply: sxt.
have uW :=inverse_V bf utx. 
have vt: inc v (target f) by apply: sxt.
set v':= Vf (inverse_fun f) v.
have vA: inc v' A by apply /(Vf_image_P fi sxs); ex_tac.
rewrite - (inverse_V bf vt) - uW - sif.
- by rewrite -Wu; move:(zle _ vA).
- rewrite sx; fprops.
- rewrite sx; fprops.
Qed.

(** The empty set is well-ordered *)

Lemma set0_or: order emptyset.
Proof. by rewrite - setI_0; apply: setIrel_or => t /in_set0. 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.  by move /setU2_eq0P => [/domain_set0_P ]. 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: diagonal (singleton x) = G. 
  apply: set1_pr; first by apply/diagonal_pi_P;fprops.
  by move => z /diagonal_i_P [pa /set1_P]; rewrite - {4} pa => -> <-.
have [pa pb] := diagonal_osr (singleton x).
have oE: (order G) by rewrite -Ei.
have sE: (substrate G = singleton x) by rewrite - Ei pb.
split =>//; apply: (worder_prop_rev oE) => y yE [z zy]; ex_tac => t ty.
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. 
have [[o1 _] s1] := (set1_wor x).
have [[o2 _] s2] := (set1_wor y).
have ta: lf_axiom (fun _ => y) (singleton x) (singleton y). 
  by move=> t;fprops.
exists (Lf (fun _ => y) (singleton x) (singleton y)).
split => //.
 rewrite s1 s2; split; aw => //.
  apply lf_bijective => //. 
    by move=> u v /set1_P -> /set1_P ->.
  move=> t /set1_P ->; exists x;fprops.
hnf; rewrite lf_source => a b  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_is0 r x: 
  order r -> substrate r = singleton x ->  r = singleton (J x x).
Proof. 
move=> or sxsu.
apply: set1_pr; first by order_tac;rewrite sxsu; fprops.
move=> v vx; move: (pr1_sr vx) (pr2_sr vx); rewrite sxsu.
move => /set1_P {2} <- /set1_P <-.  
by rewrite ((order_sgraph or) _ vx).
Qed.

Lemma set1_order_is1 r: 
  order r -> singletonp (substrate r) ->
  exists x, r = singleton (J x x).
Proof. by move=> or [x xa]; exists x; apply:set1_order_is0. 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].
rewrite(set1_order_is0 or sr); exact: (proj1(set1_wor e)).
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; first by case/set3_P; move => h;rewrite(pr1_def h)(pr2_def h); in_TP4.
case; move=> [-> ->]; apply /set3_P; in_TP4.
Qed.

Lemma cdo_glt1: glt canonical_doubleton_order C0 C1.
Proof. split; [ apply /cdo_gleP; in_TP4 | fprops]. 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: (@arg1_sr _ _ C1); apply /cdo_gleP; in_TP4.
have oc: (order canonical_doubleton_order). 
  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; [ apply:(worder_prop_rev oc); rewrite subs => x xt nex | exact].
case: (inc_or_not C0 x)=> hyp.
  ex_tac => y yx; apply /cdo_gleP; case /C2_P: (xt _  yx) => ->; in_TP4. 
move: nex=> [y yx]; ex_tac.
have p: forall t, inc t x -> t = C1.
  by move=> t tx; case/C2_P: (xt _ tx) => // ta;case: hyp; rewrite - ta.
by move => t tx; apply /cdo_gleP;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=> wor; move: (proj1 wor) => or; split=> // x y xs ys.
move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu.
have ur: sub u (substrate r) by apply: sub_set2. 
have si: substrate (induced_order r u) = u by aw.
have neu: nonempty u by ex_tac.
move: (worder_prop wor ur neu)=> [z zu zle].
move: (zle _ xu)(zle _ 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.
move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu.
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=> H As [t tA].
rewrite /has_supremum /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 => //; exact: (proj1 tA).
by move: ((proj2 H) _ 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) ->
  has_least r.
Proof. 
move=> [or wo] ne.
move: (wo  _ (@sub_refl (substrate r)) ne)=> [x]. 
by rewrite iorder_substrate //; 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=> wor nas.
have [[on sn] rd [ _ gna]]:= (order_with_greatest_pr (proj1 wor) nas).
apply:(worder_prop_rev on) => 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; case /setU1_P => // zr.
    by empty_tac1 z; apply:setI2_i.
  have ax: inc a x by rewrite xa; fprops.
  by ex_tac; rewrite xa => t /set1_P ->; order_tac; apply: xs.
have sys:sub y (substrate r) by apply: subsetI2r.
move: (worder_prop wor sys ye)=> [z zy lez].
have zx:= (setI2_1 zy).
exists z => // t tx.
move: (xs _ tx); rewrite sn; case /setU1_P => p.
  have ty: inc t y by apply: setI2_i.
  by move: (lez _ ty) => pa; apply:setU2_1.
by rewrite p; apply: gna; apply: xs.
Qed.

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

Definition Zermelo_chain E F := 
  let p :=  fun a => a -s1 (rep a) in
   [/\ 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)].

Definition worder_of E :=
  let om :=  intersection (Zo (powerset (powerset E)) (Zermelo_chain E)) in
  let d:= fun x => intersection (Zo om (sub x)) in
  let R := fun x => d (singleton x) in
  graph_on (fun x y => (sub (R y) (R x))) E.


Definition segment_r r x:= interval_cu r x.
Definition Zermelo_like r:= worder r /\ 
  forall x, inc x (substrate r) -> rep (segment_r r x) = x.

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


Lemma Zermelo_ter E (r := worder_of E):
   worder_on r E /\ Zermelo_like r.
Proof.
rewrite /r /worder_of; clear r.
set chain := (Zermelo_chain E).
set om := intersection (Zo (powerset (powerset E)) chain).
pose d p := intersection (Zo om (sub p)).
pose R x := d (singleton x).
set res:= graph_on (fun x y => (sub (R y) (R x))) E.
pose p a:=  a -s1 (rep a).
have pe: p emptyset = emptyset by apply /set0_P => x /setC_P [/in_set0]. 
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 /(sub_trans (sp A) AE). 
  move=> A AP [x xA]; move: (AP _ xA) => /setP_P xE; apply/setP_P.
  move=> t ti; exact: (xE _ (setI_hi ti xA)).
have co :chain om.
  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/Zo_hi: (yi) => / proj43;apply;apply: (setI_hi Ai yi). 
  + move=> A sAi neA;  apply: (setI_i aux) => y yi.
    by move/Zo_hi: (yi) => /proj44; apply => // t /sAi /setI_hi; apply.
move: (co)=> [sop Eo po io].
have cio: forall x, chain x -> sub om x.
  by move=> x [ha hb hc hd]; apply: setI_s1; apply: Zo_i =>//;apply /setP_P.
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; 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))) => H.
        move: H=> [x [xB xp]]; left; move=> t ti; apply:(xp _ (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: H; 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)) => H.
      move: H=> [y yA yx]; right; move => t ti;apply: (yx _ (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: H;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 X, sub X E -> inc (d X) om. 
  by move=> X XE; rewrite /d; apply: io;[ apply:Zo_S | exists E;apply: Zo_i].
have pdp: forall X, sub X E -> sub X (d X).
  rewrite /d=> X XE t tX; apply: setI_i; first by exists E; apply: Zo_i.  
  by move => y /Zo_hi; apply.
have dpq: forall X Y, inc Y om -> sub X Y -> sub X E -> sub (d X) Y.
  by rewrite /d=> X Y Yom XY XE; apply: setI_s1; apply: Zo_i.
have rdq: forall X, sub X E -> nonempty X -> inc (rep (d X)) X. 
  move=> X XE neX; case: (inc_or_not (rep (d X)) X)=>// ni. 
  have aux: (sub X (p (d X))).
    move=> t tX;apply /setC1_P; split; [ by apply: (pdp _ XE)|]. 
    move => h;case: ni; ue.
  move: (dpq _ _ (po _ (dpo _ XE)) aux XE).
  rewrite /p; case: (emptyset_dichot (d X)).
    by move => dqe; case /nonemptyP: neX; apply/sub_set0;rewrite - pe - dqe.
  by move=> ned; move: (rep_i ned) => rd dc; move: (dc _ rd) => /setC1_P [_].
have qdp: forall X Y, inc Y om -> sub X Y -> inc (rep Y) X -> Y = d X.
  move => X Y Yom sXY YX.
  have sXE: sub X E by apply: (sub_trans sXY);  apply /setP_P; apply: sop.
  apply: extensionality  =>// t tr; last by apply: (dpq _ _ Yom sXY sXE). 
  case: (st _ _  (dpo _ sXE) (po _ Yom)) => ch.
    by case /setC1_P: (ch _  ( (pdp _ sXE) _ YX)) => _.
  case: (equal_or_not t (rep Y)); first by move=> ->; apply: (pdp _ sXE).
  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]. 
  move => x xE.
  have p1: sub (singleton x) E by apply: set1_sub. 
  split; [ by apply: dpo | exact:(pdp _ p1 _ (set1_1 x)) | ].
  exact:(set1_eq (rdq _ p1 (set1_ne x))).
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 X, inc X om -> nonempty X -> R (rep X) = X. 
  move=> X Xom neX; 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.
  by rewrite (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4).
have [or sr]:order_on res E.
  split; last by apply: graph_on_sr => a _.
  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.
  + by move => u ue.
have wor:worder res.
  apply:(worder_prop_rev or)=> x; rewrite sr => xsr nex.
  move:(rdq x xsr nex) => rdx.
  ex_tac=> a ax; 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). 
split=>//;split=>//; rewrite sr -/res => x xE.
suff: (segment_r res x) = R x by move => ->; exact:(proj33 (Rp _ xE)).
set_extens t.
  move /segment_rP /(graph_on_P0 (fun x y=> sub (R y) (R x)) E x t).
  move => [_ tE ]; apply; exact (proj32 (Rp _ tE)).
move => tR; move: ((setP_hi (sop _ (proj31 (Rp _ xE)))) _ tR) => tE.
by apply/segment_rP; apply/graph_on_P1; split => //; apply: sRR.
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.
have injf:= (total_order_monotone_injective to sm).
have injg:= (total_order_monotone_injective to smg).
move:sif sig=> [or or' [ff sr sr'] si] [_ _ [fg srg sr'g] sig] rr {sm smg}.
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:(worder_prop wo Asf eA)=> [x 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=> /xl hh; 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 _].
  suff: inc z A by move=> /xl h'; order_tac.
  by apply: Zo_i=>//; rewrite -WWw;  dneg xx; apply: (proj2 injg).
order_tac.
Qed.

Lemma iso_unique r r' f f': 
  worder r -> order_isomorphism f r r' ->  order_isomorphism f' r r' ->
  f = f'.
Proof.
move => wor ha hb.
have ha':= (order_isomorphism_increasing ha).
have hb':= (order_isomorphism_increasing hb).
have hd: range (graph f) = range (graph f').
  move: ha => [_ _ [[_ /surjective_pr3 ->] _ ->] _]. 
  by move: hb => [_ _ [[_ /surjective_pr3 ->] _ ->] _]. 
apply(strict_increasing_extens ha' hb' wor hd).
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).
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_S. 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. by move=> t /Zo_hi [/setI2_2 /setXp_P [] ]. Qed.

Lemma segment_inc r x y: glt r y x -> inc y (segment r x). 
Proof. move=> xy;apply /Zo_i =>//;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_S. 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. 
hnf; move: sis; rewrite /segmentp; aw.
move=> [s's hyp]; split; first 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) => 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. by 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. 
have tor := (worder_total wor); have or := proj1 tor.
have sys: (sub y (substrate r)) by apply: sub_setC.
move: (worder_prop wor sys ney)=> [x 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) => //.
  by case /setC_P: xy => [_  bad]  /(proj2 sr _ _ zs).
ex_middle zis.
have zy: (inc z y) by apply/setC_P; split => // ;apply: (sub_segment zs).
move: (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: (worder_least wo sre) => [a lea] [x xsr p]. 
right; exists x, 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.
by 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.
by 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 (E := substrate r)(A := union (segmentss r)):
   total_order r ->
   ( (forall x, ~ (greatest r x)) -> A = E)
   /\ (forall x, greatest r x -> A = E -s1 x).
Proof.
move=> tor.
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 => /Ap [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.
by apply/Ap; exists x; split=>//; 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 : total_order r ->
  {inc (substrate r) &,  injective (segment r) }.
Proof.
move=> tor x y 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.
have p3:= (segment_monotone1 tor xsr ysr p1).
have p4:= (segment_monotone1 tor ysr xsr p2).
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].
hnf; 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.
hnf; aw;move=> x y xsr ysr; aw; split.
  move=> hyp; apply/sub_gleP;split => //; fprops.
  by apply: segment_monotone. 
move /sub_gleP=> [_ _ ss].
exact: (segment_monotone1 (worder_total wor) xsr ysr ss).
Qed.


Theorem segments_worder r: worder r ->
  worder (sub_order (segments r)).
Proof. 
move=> wor; move: (wor)=> [or _];move: (worder_total wor)=> tor.  
have [oi sr] := (sub_osr (segments r)).
apply:(worder_prop_rev oi); rewrite sr => x xsr nex.
set y := x \cap (segmentss r).
case: (emptyset_dichot y) => hy.
  have xv: x = singleton (substrate r).
    apply: set1_pr1=>// z zx.
    case /setU1_P: (xsr _ zx) => //.
    by move=> aux; empty_tac1 z; apply: setI2_i.
  have srx: inc (substrate r) x by rewrite xv; fprops.
  by ex_tac; rewrite xv; move=> z /set1_P ->; order_tac;rewrite sr; apply:xsr.
have ysr: sub y (segmentss r) by move => t ty; apply: (setI2_2 ty).
have segp a: inc a y -> exists2 u, inc u (substrate r) & a = segment r u.
   by move=>  /ysr /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].
   have  <- //: u = cf a.
   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: (worder_prop wor zsr nez) => [a 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/sub_gleP; split; fprops.
case /setU1_P: (xsr _ bx); [ move => h | by move=>->; apply: sub_segment ].
have biy: (inc b y) by apply: setI2_i.
have cbz: (inc (cf b) z) by apply /funI_P; ex_tac.
move: (lea _ cbz).
by move: (cfp _ biy)=> [p1 {2} ->]; 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 => 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 hnf; rewrite su.
    rewrite /related => x y z p1 p2.
    move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]].
    move: (alo _ cdg) => or; rewrite /G /related; union_tac; order_tac.
  rewrite /related => 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 apply:(sub_graph_coarse_substrate ga).
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:= (proj41 or _ xr).
move:(pr1_sr xr)(pr2_sr xr); rewrite sr => 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 p0 a x y: inc x (substrate (Vg g a)) -> gle G y x -> inc y (substrate G)
   -> inc a (domain g) -> inc y (substrate (Vg g a)).
  move => xs yx ys adg.
  move: (setUf_hi yx) => [u udg Jv].
  case: (pc  _ _ adg udg) => h; first by apply:(proj1 h); substr_tac.
  exact: (proj2 h _ _ xs Jv).
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;exact: (p0 a _ _ xs yx (arg1_sr yx) adg).
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 => //;rewrite (Vag _ adg);apply/iorder_gleP => //.
  exact: (p0 a _ _ xs yx (arg1_sr yx) adg).
have p4: (forall a x, inc a (domain g) -> segmentp (Vg g a) x -> 
    segmentp G x).
  move=> a x adg sa; case: (well_ordered_segment (pb _ adg) sa).
    by move=> ->; apply: p2.
  move=> [y ysV ->]; rewrite (p3 _ _ adg ysV); apply: segment_segment=>//. 
  by apply: (p1 _ adg).
have p5: worder G.
  apply:(worder_prop_rev oh) => 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: (worder_prop (pb _ adg) sx1s nx1)=> [z 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 => // t tx.
  move: (xsr _ tx); rewrite sh => tu; move: (setUf_hi tu)=> [b bdg bV]. 
  have aux: inc t (substrate (Vg g a)) -> gle G z t.
    move=> hyp.
    by move:(zle _ (setI2_i tx hyp));rewrite (Vag _ adg) => /iorder_gle1. 
  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 => //. 
exact (proj1 (pb _ adg)).
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.
Hypothesis adj_stable:
 (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 case: 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: (scs); rewrite - {1} sr1 => src1.
move:(worder_prop woi src1 necs) => [y ycs hyp].
move/setC_P:(ycs) => [yssr nys].
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: (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, ~ 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: (hyp _ zcs) => /sub_gleP [_ _ yz].
  move: uy; aw => uy; move: (yz _ uy).
  by rewrite zv=>/not_in_segment.
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 case: wor.
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 by apply:corresp_s.
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 /=.
set si := Lg s id.
set t:= unionf _ _. 
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 _].
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.
  hnf; rewrite (slso _ ins); aw; split => //.
  apply: function_pr; fprops.
    apply: (@sub_trans (target (tdf i))); first by apply: f_range_graph. 
    rewrite /t => x xt; union_tac.
  by rewrite (f_domain_graph fd) (slso _ ins).
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))). 
    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]. 
  hnf; 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].
have sjf: surjection f.
  split => //; rewrite gf /t => y 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.
split => //; split => //; first  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; hnf; apply: not_in_segment.
set (h:= (restriction_to_segment r x g)).
have sto := (extension_fs (p h) (proj1 sug) nxsg sug).
have tos:(segment r x) +s1 x = tsx by rewrite /tsx segmentc_pr//. 
have soto: source (extension g x (p h)) = tsx.
  by rewrite/extension; aw; rewrite sog.
hnf;rewrite sioc; split => // y ytsx.
have syx: (sub (segment r y) (segment r x)).
  by move: ytsx => /segmentcP; apply: segment_monotone.
have fto: function (extension g x (p h)) by fct_tac.
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. 
  congr p.
  apply: rts_extensionality =>//; aw; try ue.
    rewrite soto p2; fprops.
  hnf; 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 apply: choose_pr;  exists x. 
apply: (transfinite_unique wo tdt td).
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 [ ext _].
by apply:choose_pr.
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 => wor hb t.
have or := proj1 wor.
move:(transfinite_defined_pr p wor); set f := transfinite_defined r p.
move => [sfj sf frec]; move/(proj2 sfj); rewrite sf; move => [x xsf <-].
move: x xsf.
apply:(transfinite_principle wor) => x xsr xrec; rewrite (frec _ xsr).
have ssa: sub (segment r x) (source f) by rewrite sf; apply:sub_segment.
move:(rts_fs (proj1 sfj) ssa) => [fg _].
apply: hb => //.
  by rewrite /restriction_to_segment/restriction1; aw; apply:segment_segment.
rewrite /restriction_to_segment/restriction1; aw.
move => y /(Vf_image_P (proj1 sfj) ssa) [u /segmentP ua ->]; apply: xrec => //.
order_tac.
Qed.


Theorem transfinite_definition_stable_orig 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 x: inc x s -> segmentp r x by move/Zo_S /(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.


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 = Vfs 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 = Vfs 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: fterm):
  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 x xX.
have srr: sub (substrate r) (substrate r) by []. 
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.
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. 
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 pb;apply:setI2_i => //; apply:setXp_i;apply/segmentP =>//.
    order_tac.
apply: Zo_i; [ fprops | 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]. 
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 -pt eq;  order_tac.
move=> neq; rewrite -pt in tr.
have: inc (P t) (segment r (Q t)) by apply: segment_inc.
rewrite ss  -{3} pt => aux.
exact: (proj1 (inc_segment aux)).
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: (iorder_gle1  (px _ zc)) => h; order_tac.
  apply /segmentP.
  case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz.
  case: xc; exact: ((proj2 svr) _ _ 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: (iorder_gle1 (py _ zc)) => h; order_tac.
  apply /segmentP.
  case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz.
  case: yc; exact: ((proj2 svr') _ _ zs yz).
have xy: x = y by rewrite - (pr _ xs) -(pr' _ ys) p1 p2.
case: xc.
apply: Zo_i; first by apply :setI2_i => //; ue.  
by rewrite p1 xy p2. 
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:(worder_adjoin_greatest wor nas) => woe.
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 xna]. 
     have: inc x (substrate owg) by order_tac.
     by 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/iorder_gleP => //.
move: (arg1_sr yx); rewrite se => /setU1_P; case => // eya.
move: (prop _ xsre); rewrite -/owg - eya => xy; case: nyx; 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 hnf; 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 ].
  hnf; 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.
  hnf;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 Vga a: inc a m -> Vg g a = a by move=> am; rewrite /g; bw.
move: coex => [om0 som0 pom0].
rewrite dg in alsu ssu ssup  som0 pom0.
set (m0:= unionb g). 
have Za: (Zermelo_axioms E p s m0).
  hnf; split => //; rewrite som0=> t tu;move: (setUf_hi tu)=> [u ud ts];
     move: (ud) => /Zo_P [_ [_ p1 p2 p3]];
     move: (ts); rewrite Vga // => tb.
      by apply: p1.
    by rewrite -(ssu _ _ ud ts); rewrite Vga //; apply: p2.
  by rewrite -(ssu _ _ ud ts); rewrite Vga //; apply: p3.
exists m0 => // sm0s.
move:(pp _ sm0s)=> [pE nps]. 
move: (Zermelo_aux4 wou nps) => [woe seu asu].
set (a:= p (substrate m0)).
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].
  have H t: inc t (substrate m0) ->
      segment (order_with_greatest (unionb g) a) t = segment (unionb g) t.
    move => ts; move: (setU1_r (p (substrate m0)) ts); rewrite - su => /asu.
    by case => // hyp; case: nps; rewrite - hyp.
  split=>//;  rewrite su => t /setU1_P; case.
  - apply: p2.
  - by move=> ->.
  - by move=> ts; rewrite (H _ ts); apply: p3.
  - by move => ->; rewrite seu.
  - by move=> ts;rewrite (H _ ts); apply: p4.
  - by move=> ->; rewrite seu.
have um:inc (order_with_greatest m0 a) m. 
  apply: Zo_i =>//;apply /setP_P.
  apply: sub_trans (setX_Sll (proj42 Zae)).
  apply: sub_graph_coarse_substrate; fprops. 
case: nps; rewrite {2} som0.
apply: (setUf_i um); rewrite (Vga _ um) 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.
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.
by apply/setC_P; split; [ apply /setP_P | 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)  => /sfunctionsP [].
have Hb:forall i, inc i X -> target i = b. 
  by move=> i iX; move: (Xs _ iX)  => /sfunctionsP [_ ].
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; [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; hnf; 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 /sfunctionsP;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) =>  /sfunctionsP [_ 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 => //.
apply/(sub_functionP fy fg).
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)).
  by move=> x xs; move: (apx _ xs); rewrite /px; move=> [[h1 h2] h3].
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')).
  move=> x xr.
  move:(pr1_sr xr)(pr2_sr xr) => Ps Qs.
  have gr: sgraph r' by fprops.
  move: (gr _ xr) => xp; rewrite -xp; rewrite - xp in xr.
  case: (equal_or_not (P x) (Q x)) => aux. 
    rewrite aux; order_tac; aw.
  have ltPQ: glt r' (P x) (Q x) by split.
  have Pse: (inc (P x) (segment r' (Q x))) by apply/segmentP.
  apply /iorder_gleP => //.
  by move: (alse _ Qs)(ps _ Qs) => p1 <-; apply: (proj2 (proj1 (apx _ p1))).
have r'v: r' = induced_order r (substrate r').
  apply: extensionality => // 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. 
  move:(pr1_sr tio)(pr2_sr tio); rewrite sr1 => Ps Qs.
  rewrite -pt in tio |- *.
  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 => // x ux.
ex_middle h.
have xu: (glt r u x) by split => //; apply: nesym.
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; hnf;  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)(gle r a)).
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.
suff isF: inductive (induced_order r F).
  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. 
move=> u; aw=> uF; rewrite iorder_trans // => toi.
have tos: (sub (u +s1 a) (substrate r)).
  by apply: sub_trans Fs => 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 u a)) => ab.
have bF: inc b F by rewrite /F; apply: Zo_i. 
exists b; split; aw=>// y yu.
by move: (bub _  (setU1_r a yu)) => yb; apply/iorder_gleP => //; apply: uF.
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.
have p1: inc (union X) A.
  apply: Sp =>// x y xX yX.
  case: (tX _ _ xX yX).
   by move/iorder_gle1 => /sub_gleP [_ _ h]; left.
   by move/iorder_gle1 => /sub_gleP [_ _ h]; right.
exists (union X);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 =>// 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) ha. 
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 (substrate r) by rewrite /s sf; apply: Zo_S.
move:(worder_prop wor ssf nes)=> [y ys yle].
move: ys => /Zo_P [ysf [leWy neWy]].
have Wrg: inc (Vf f y)  (range (graph f)) by Wtac. 
move: ((proj2 sr) _ _ Wrg leWy).
move/(range_fP ff) => [z zf vv].
have lt1: glt r' (Vf f z) (Vf f y) by rewrite - vv.
have lt2: glt r z y.  
   have: (glt r z y \/ gle r y z).
     rewrite sf in ysf zf; apply: (total_order_pr2 tor zf ysf). 
  case =>// 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 apply: Zo_i. 
  case: (not_le_gt or (yle _ zs)  lt2).
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 =>//.
      by hnf; 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 hnf;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 => /sfunctionsP [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]].
(* maybe f is the answer *) 
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')).
(* first case is excluded; uniqueness is trivial *)   
right; apply /unique_existence;split; last first.
  move=> a b [s1 m1][s2 m2].
  by apply: (isomorphism_worder_unique (r:=r') (r':=r)) =>//.  
(* maybe the inverse of f is the answer *)
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.
  hnf; rewrite rgg /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.
(*  Here f is not maximal, we construct an extension *)
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 apply: extension_f. 
have tg: target g = E'.  
  rewrite/g /extension; aw; rewrite tf;  by apply: setU1_eq.
have sg: source g = segmentc r a.
  by rewrite /g/extension; aw; rewrite sfx xa; apply: segmentc_pr.
have sap t: sub (segmentc r t) (substrate r)  by 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/sfunctionsP;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.
  hnf;split => // u v; rewrite sg - 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 //].
      move:(isf u v hu hv). move:(iff_sym(iorder_gleP r hu hv)); rewrite sfx.
      move => qa qb; exact: (iff_trans qa qb).
     by move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _].
  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.
(* We express maximality *)
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.
  by apply /extension_orderP.
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 split => //; ue.
have cf'f: (f' \coP f) by split => //; ue.
have mor1 := (compose_order_morphism om' om).
have mor2 := (compose_order_morphism om om').
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] yx.
  have xrg: (inc x (range (graph f'))) by ex_tac.
  have usr: inc u (source f') by Wtac.
  move: ((proj2 sr2) _ _  xrg yx) => /(range_fP ff') [v vsf' vp].
  move: yx; rewrite (Vf_pr ff' p2) vp -fp'// => yr.
  move: ((proj2 sr1) _ _  urg yr) => va; apply /dirim_P; ex_tac; Wtac.
have srg': segmentp r' (range (graph (f \co 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] yx.
  have xrg: (inc x (range (graph f))) by ex_tac.
  have usr: inc u (source f) by Wtac.
  move: ((proj2 sr1) _ _  xrg yx) => /(range_fP ff) [v vsf' vp].
  move: yx; rewrite (Vf_pr ff p2) vp -fp// => yr.
  move: ((proj2 sr2) _ _  urg yr) => va; apply /dirim_P; ex_tac; Wtac.
have p1 := (unique_isomorphism_onto_segment wor srg mor2).
have p2 := (unique_isomorphism_onto_segment wor' srg' mor1).
rewrite - sf in p1; rewrite - sf' in p2.
have [p3 p4 p5] := (bijective_from_compose cff' cf'f  p2 p1).
by 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.
have woi :=(induced_wor wo asr).
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 case: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.
  hnf; 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). 
    split => //; split => //;last by rewrite -hyp tf.
    split=>//; apply: surjective_pr4 =>//. 
  have ioi :=(inverse_order_is oi).
  exists (substrate r); exists (inverse_fun f). 
  split; first by apply: substrate_segment. 
  by 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 => //.
  apply:iorder_gle2 (inc_segment Ws).
have ssf: sub s (substrate r) by rewrite - sf;apply: Zo_S. 
move: (worder_prop wo ssf nes) => [y 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: (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.
move => [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/(proj2 sjf) =>[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; hnf; 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).
  hnf; split => //; rewrite /g; aw.
     split; aw.
  hnf; aw; move=> x y xB yB /=; aw.
  move:(iorder_gleP r (ta _ xB) (ta _ yB)) => xx.
  hnf 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 => f1a f2a.
  apply: (iff_trans (iorder_gleP r f1a f2a)).
  by symmetry.
have wob:= (induced_wor woa Bs).
have gi:= (unique_isomorphism_onto_segment wob sr om).
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; 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 => //. 
    hnf;  rewrite qb /restriction1; aw; split => //.
       by apply: restriction1_fb.
    by rewrite -rgx - image_by_fun_source. 
  hnf; 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; 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)); split => //.
  rewrite qb /restriction1; split; aw; first by apply: restriction1_fb => //.
  by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
hnf; 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.


Lemma isomorphism_worder3 r r': worder r -> worder r' ->
  (exists f, segmentp r' (range (graph f)) /\ order_morphism f r r')
  \/ (exists2 x, inc x (substrate r) & (induced_order r (segment r x)) \Is r'). 
Proof.
move => wor wor'.
case: (isomorphism_worder wor wor').
  by move => [f [fa _ ]]; left; exists f.
move=> [f [[fa fb] _ ]].
move: (order_morphism_fi fb) => injf.
move: fb => [or' or [ff pd pe] pf].
case : (well_ordered_segment wor fa) => eq1.
  left; exists (inverse_fun f).
  have bf: bijection f.
    by split => //; apply: (surjective_pr4 ff); rewrite pe.
  rewrite {1} /inverse_fun corresp_g (igraph_range (function_sgraph ff)).
  rewrite(f_domain_graph ff) pd; split; first by apply: substrate_segment.
  have fif:= (bijective_inv_f bf).
  have sfi: source f = target (inverse_fun f) by aw.
  have tfi: target f = source (inverse_fun f) by aw.
  split => //; [ by split; aw |  move => x y; aw => xtf ytf ].
  rewrite - {1} (inverse_V bf xtf) - {1} (inverse_V bf ytf).
  apply: iff_sym;apply:  pf; rewrite sfi; Wtac; aw.
move: eq1 => [x xsr rgx]; right;ex_tac; apply: orderIS.
move: (@sub_segment  r x) => p1.
move: (iorder_osr or p1) => [qa qb].
exists (restriction1 f (source f)); split => //.
  rewrite qb /restriction1; split; aw;first by apply: restriction1_fb => //.
  by rewrite /restriction1; aw; rewrite -rgx -image_by_fun_source.
hnf; rewrite {1 2} /restriction1; aw; move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_V ff ssf ax) (restriction1_V ff 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).


(** Alternate formulation without [least_element] *)

Lemma orprod_gle1P r g:
  orprod_ax r g -> forall x x',
  (related (order_prod r g) x x' <-> 
  [/\ inc x (prod_of_substrates g),  inc x' (prod_of_substrates g) &
    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)]).
Proof. move=> ax x x';apply/graph_on_P1. Qed.

Lemma orprod_gleP r g :  orprod_ax r g -> forall x x',
  (gle (order_prod r g) x x' <-> 
  [/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) &
    (x= x' \/ exists j, [/\ inc j (substrate r),
      glt (Vg g j) (Vg x j) (Vg x' j) &
      forall i, glt r i j -> Vg x i = Vg x' i])]).
Proof. 
move=> la x x'.
move: (la) => [wor sr alo]; move: (proj1 wor) => or.
have He: domain (fam_of_substrates g) = domain g. 
  by rewrite /fam_of_substrates; bw.
have Hf: fgraph(fam_of_substrates g) by rewrite /fam_of_substrates; fprops.
split. 
  move/(orprod_gle1P la) => [xp x'p aux]; split => //.
  set (s := (Zo (domain g) (fun i => Vg x i <> Vg x' i))) in aux.
  have ssr: sub s (substrate r) by rewrite sr; apply: Zo_S.
  case: (emptyset_dichot s)=> nse. 
    left; apply: (setXb_exten xp x'p). 
    move=> i idf; ex_middle h; empty_tac1 i. 
    by rewrite /s; apply: Zo_i;  move: idf; rewrite /fam_of_substrates; bw.
  have [j jle] := (proj2 wor _ ssr nse).
  have jp :=(aux _ jle).
  move: jle => []; aw;move=> js jmin.
  have jsr: inc j (substrate r) by apply: ssr.
  right; exists j; split => //; move=> i ij;  ex_middle v. 
  have iis : (inc i s) by rewrite /s; apply: Zo_i =>//;rewrite - sr;order_tac.
  move: (iorder_gle1 (jmin _ iis)) => aux'; order_tac.  
move => [xp x'p aux]; apply /(orprod_gle1P la);split => //.
set s := (Zo (domain g) (fun i  => Vg x i <> Vg x' i)). 
have ssr: (sub s (substrate r)) by rewrite sr; apply: Zo_S.
move=> j []; aw; move => js jmin.
move /Zo_P: js =>[jdg Vj].
case: aux => haux; first by rewrite haux in Vj. 
have [i [isr lti aeq]] := haux.
have iis: inc i s by move:lti => [_ ok];apply: Zo_i =>//; ue. 
have ij := (iorder_gle1 (jmin _ iis)).
case: (equal_or_not j i) => ji; first by ue. 
have ltji: glt r j i by split.
by case: Vj; apply: aeq.
Qed.


Lemma orprod_osr r g:
  orprod_ax r g -> order_on (order_prod r g) (prod_of_substrates g).
Proof.
move => ax; move: (ax)=> [wor sr ao].
have osr: substrate (order_prod r g) = prod_of_substrates g.
  rewrite /order_prod graph_on_sr //.
  move=> x _ j [js _]; move: js; aw; fprops; last by rewrite sr; apply: Zo_S.
  by move /Zo_hi; case.
split => //.
have tor: total_order r by apply: worder_total.  
split.
+ by apply: graph_on_graph.
+ by hnf; rewrite osr => y ya; apply/(orprod_gleP ax); split => //; left.
+ move => v u w ha.
  move/(orprod_gleP ax): (ha) => [ux _]; case; first by move ->.
  move => [j1 [j1sr hu1 hu2]].
  move/(orprod_gleP ax) => [_ wx]; case;first by move <-.
  move => [j2 [j2sr hv1 hv2]]; apply/(orprod_gleP ax); split => //; right.
  case (equal_or_not j1 j2) => j12.
    exists j1; rewrite - j12 in hv1 hv2; split => //.
      rewrite sr in j1sr; exact:(lt_leq_trans (ao j1 j1sr) hu1 (proj1 hv1)).
    by move => i ha1; rewrite (hu2 _ ha1) (hv2 _ ha1).
  case:(proj2 tor _ _ j1sr j2sr) => h.
    exists j1; split => //; first by rewrite - (hv2 _ (conj h j12)).
    by move => i ia;rewrite  (hu2 _ ia) (hv2 _ (lt_leq_trans (proj1 wor) ia h)).
  exists j2; split => //; first by rewrite (hu2 _ (conj h (nesym j12))).
  by move => i ia; rewrite - (hv2 _ ia) (hu2 _ (lt_leq_trans (proj1 wor) ia h)).
move => u v.
move/(orprod_gleP ax) => [_ _]; case => // [[j1 [j1sr hu1 hu2]]].
move/(orprod_gleP ax) => [_ _]; case => // [[j2 [j2sr hv1 hv2]]].
case: (equal_or_not j1 j2) => sj.
  move: hv1 => []; rewrite - sj => hv11; rewrite sr in j1sr.
  by rewrite(order_antisymmetry (ao j1 j1sr) (proj1 hu1) hv11).
case:(proj2 tor _ _ j1sr j2sr) => h.
  by move: (hv2 _ (conj h sj)) (proj2 hu1) => ->.
by move:(hu2 _ (conj h (nesym sj))) (proj2 hv1) => ->.
Qed.

Lemma orprod_sr r g:
  orprod_ax r g -> substrate(order_prod r g) = prod_of_substrates g.
Proof. move => h;exact: (proj2 (orprod_osr h)). Qed.

Lemma orprod_or r g:
  orprod_ax r g -> order (order_prod r g).
Proof. move => h;exact: (proj1 (orprod_osr h)). Qed.

(** A product of total orders is total *)

Lemma orprod_total r g:
  orprod_ax r g ->
  (allf g total_order) ->
  total_order (order_prod r g).
Proof. 
move=> la alt.
have [ol sl] := (orprod_osr la).
have [[or wor] sr ao] := la.
split=>//; rewrite sl; move=> x y xsr ysr.
have fgf:fgraph (fam_of_substrates g) by rewrite/fam_of_substrates; fprops.
set s:=(Zo (substrate r) (fun i => Vg x i <> Vg y i)).
case: (emptyset_dichot s) => nse.
  suff xy: x = y by left; rewrite xy; order_tac; rewrite sl.
  apply: (setXb_exten xsr ysr).
  move=> i idg; ex_middle u;empty_tac1 i.
  by rewrite/s; apply: Zo_i; move: idg; rewrite/fam_of_substrates; bw; ue. 
have ssr: sub s (substrate r) by rewrite/s; apply: Zo_S. 
have  [j jle] := (wor _ ssr nse).
move: (jle)=> [];rewrite iorder_sr // => js jp.
have jdg: inc j (domain g) by rewrite - sr; apply: ssr. 
have [orj torj] := (alt _ jdg).
have px: (inc (Vg x j) (substrate (Vg g j))) by apply:prod_of_substrates_p.
have py: (inc (Vg y j) (substrate (Vg g j))) by apply:prod_of_substrates_p.
  move:ysr; rewrite /prod_of_substrates/fam_of_substrates; aw.  
have [ois sir] :=(iorder_osr or ssr). 
move: js => /Zo_hi  h h'.
case: (torj _ _ px py) => leaux.
  left; apply /(orprod_gle1P la); rewrite - sr; split => // k kl.
  rewrite - (unique_least ois jle kl); split =>//.
right; apply /(orprod_gle1P la); split => //.
have <-: s=(Zo (domain g) (fun i => Vg y i <> Vg x i)). 
   rewrite /s sr; set_extens t; move/Zo_P => [pa pb]; apply: Zo_i; fprops.
move => k kl.
by rewrite - (unique_least ois jle kl); split =>//; apply /nesym.
Qed.

(** Disjoint union of families of substrates *)

Definition sum_of_substrates g := disjointU (fam_of_substrates g).

Lemma du_index_pr1 g x: inc x (sum_of_substrates g) ->
  [/\ inc (Q x) (domain g), inc (P x) (substrate (Vg g (Q x))) & pairp x].
Proof. 
move=> xdu; move :(disjointU_hi xdu) => [].
by rewrite fos_d => h; bw => h1; split.
Qed. 

Lemma disjoint_union_pi1 g x y:
  inc y (domain g) -> inc x (substrate (Vg g y)) ->
  inc (J x y) (sum_of_substrates g). 
Proof. move=> ydg xsv; apply: disjointU_pi; bw. Qed.

Lemma canonical2_substrate r r':
  fam_of_substrates (variantLc r r') = variantLc (substrate r) (substrate r').
Proof. 
rewrite /fam_of_substrates /variantLc.
  apply: fgraph_exten; fprops; bw. 
move=> x xtp;  try_lvariant xtp;  fprops. 
Qed.

(** ordinal sum of a family of orders g indexed by the substrate of r *)

Definition orsum_ax r g:=
  [/\ order r, substrate r = domain g & order_fam g].

Definition order_sum_r r g x x' := 
    (glt r (Q x) (Q x') \/ (Q x = Q x' /\ gle (Vg g (Q x)) (P x) (P x'))).

Definition order_sum r g := 
  graph_on (order_sum_r r g) (sum_of_substrates g).

Section OrderSumBasic.
Variables r g: Set.
Hypothesis osa: orsum_ax r g. 

Lemma orsum_gleP x x': gle (order_sum r g) x x' <->
  [/\ inc x (sum_of_substrates g), inc x' (sum_of_substrates g) &
    order_sum_r r g x x'].
Proof. apply: graph_on_P1. Qed.

Lemma orsum_gle1 x x':
  gle (order_sum r g) x x' ->
  (glt r (Q x) (Q x') \/ (Q x = Q x' /\ gle (Vg g (Q x)) (P x) (P x'))).
Proof. by move /orsum_gleP => [_ _].  Qed.

Lemma orsum_gle2 a b a' b':
  gle (order_sum r g) (J a b)(J a' b') ->
  (glt r b b' \/ (b = b' /\ gle (Vg g b) a a')).
Proof. move => h2; move:(orsum_gle1 h2); aw. Qed.

Lemma orsum_gle_id  x x':
  gle (order_sum r g) x x' -> gle r (Q x) (Q x').
Proof.
move /orsum_gleP => [xs _ ] [] [] => // <- _. 
move: (du_index_pr1 xs)=> [qd _ _].  
move: osa => [or srdg _]; order_tac; ue.
Qed.

Lemma orsum_or: order (order_sum r g).
Proof. 
move: osa=> [or sr alo].
rewrite /order_sum; set s := _ r g; set x:= _ g.
have ->: (graph_on s x = graph_on (fun a b => [/\ inc a x, inc b x & s a b]) x).
  by apply : Zo_exten1 => t /setX_P [_ pa pb]; split => //;move => [_ _].
apply: order_from_rel; split => //; rewrite /s/order_sum_r.
- move=> u v w [ux vx suv] [_ xw suw];split => //.
  case: suv; case: suw.
  + by left; order_tac.
  + by move=> [sq leq]; rewrite sq; left.
  + by move=> h [sq leq]; rewrite sq;left.
  + move=> [sq1 le1][sq2 le2]; right; split; first by ue. 
    move: (du_index_pr1 ux) => [qdg _ _].
    by rewrite  - sq2 in le1; move: (alo _ qdg)=> ov;  order_tac.
- move=> u v [ux vx suv] [_ _ svu]. 
  have [qudg puv pu] := (du_index_pr1 ux).
  have [qvdg pvv pv] := (du_index_pr1 vx).
  case: suv; case: svu.
  + move=> lt1 lt2; order_tac.
  + by move => [eq _] [_ lt1]; case: lt1.
  + by move => [_ lt1]  [eq _]; case: lt1.
  + move=> [eq le1][_ le2]; rewrite eq in le1; move: (alo _ qudg) => ou. 
    apply: pair_exten =>//;order_tac.
- move=> u v [ux vx suv].
  have [qudg puv pu] := (du_index_pr1 ux).
  have [qvdg pvv pv] := (du_index_pr1 vx).
  by split; split => //;right; split => //;
     [move: (alo _ qudg) | move: (alo _ qvdg) ] => ou; order_tac.
Qed.

Lemma orsum_sr: substrate (order_sum r g) = sum_of_substrates g.
Proof. 
rewrite /order_sum graph_on_sr // =>  a asg.
have [qudg puv pu] := (du_index_pr1 asg).
by right; split => //;move: osa =>[_ _ alo];move: (alo _ qudg) => ou; order_tac.
Qed.

Lemma orsum_osr: order_on (order_sum r g) (sum_of_substrates g).
Proof. by split; [apply: orsum_or | rewrite orsum_sr]. Qed.

End OrderSumBasic.

Hint Resolve orsum_or orprod_or: fprops.
Hint Rewrite orsum_sr orprod_sr : bw.

Definition order_prod2 r r' :=
  order_prod canonical_doubleton_order (variantLc r' r).

Definition order_sum2 r r' :=
  order_sum canonical_doubleton_order (variantLc r r').

Lemma order_sp_axioms r r': 
  order r -> order r' -> order_fam  (variantLc r r').
Proof. 
move => or or';hnf; bw;move=> i itp; try_lvariant itp.  
Qed.

Hint Resolve order_sp_axioms: fprops.

Section OrderSum2Basic.
Variables r r': Set.
Hypotheses (or: order r) (or': order r').

Lemma orsum2_osr: 
  order_on (order_sum2 r r') (canonical_du2 (substrate r) (substrate r')).
Proof.
move: cdo_wor => [[ord _ ] sr].
have aw: orsum_ax canonical_doubleton_order (variantLc r r').
   by  split => //; bw; fprops.
split; first by apply: orsum_or.
rewrite  orsum_sr // /canonical_du2 /order_sum2 /sum_of_substrates. 
rewrite canonical2_substrate //.  
Qed.

Lemma orprod2_osr: 
  order_on (order_prod2 r r')(product2 (substrate r')  (substrate r)).
Proof.
have [wor sr] := cdo_wor.
have aux: orprod_ax canonical_doubleton_order (variantLc r' r).
  by split => //; bw; fprops.
split; first by apply: orprod_or.
rewrite /order_prod2 orprod_sr // /prod_of_substrates canonical2_substrate //.
Qed.

Lemma orsum2_or: order (order_sum2 r r').
Proof. exact: (proj1 orsum2_osr). Qed.

Lemma orsum2_sr: 
  substrate (order_sum2 r r') = canonical_du2 (substrate r) (substrate r').
Proof.  exact: (proj2 orsum2_osr). Qed.


Lemma orprod2_or: order (order_prod2 r r').
Proof. exact: (proj1 orprod2_osr). Qed.

Lemma orprod2_sr: 
  substrate(order_prod2 r r') = product2 (substrate r')  (substrate r).
Proof. exact: (proj2 orprod2_osr). Qed.


Lemma orsum2_gleP x x':
  gle (order_sum2 r r') x x' <->
  [/\ inc x (canonical_du2 (substrate r) (substrate r')),
    inc x' (canonical_du2 (substrate r) (substrate r')) &
    [\/ [/\ Q x = C0, Q x' = C0 & gle r (P x) (P x')],
        [/\ Q x <> C0, Q x' <> C0 & gle r' (P x) (P x')] |
        (Q x = C0 /\ Q x' <> C0)]].
Proof. 
have Ha: C1 <> C0 by fprops.
set S1:= (canonical_du2 (substrate r) (substrate r')).
have S1p: S1 =  (sum_of_substrates (variantLc r r')).
  by rewrite /sum_of_substrates  canonical2_substrate.
split. 
  move /orsum_gleP; rewrite - S1p.
  move=> [xs xns' osr]; split => //; move: osr => [] [].
    move /cdo_gleP => aux nsQ;case: aux.
      by move=> [e1 e2];  rewrite e1 e2 in nsQ;case: nsQ.
    case; first by move=> e1 e2; rewrite e1 e2 in nsQ; case: nsQ.
    move=> [e1 e2];  constructor 3; rewrite e2; split => //.
  move=> <-.
  case: (candu2_pr2 xs) => ->; bw; [constructor 1| constructor 2]; split => //. 
move=> [xs1 x's1 etc]; apply/orsum_gleP; split => //; try ue.
case: etc.
   move=> [qxa qx'a lrxx']; right; rewrite qxa qx'a; bw;split => //.
  move=> [qxa qx'a lrxx']; right.
  have ->:  (Q x' = C1) by case: (candu2_pr2 x's1) => //.
  have ->:  (Q x = C1)  by case: (candu2_pr2 xs1) => //.
  bw; split => //.
move=> [qxa qx'a]; left; rewrite qxa.
have ->: Q x' = C1 by case: (candu2_pr2 x's1) => //.
apply: cdo_glt1.
Qed.

Lemma orsum2_gle_spec x x':
  inc x (substrate r) -> inc x' (substrate r') ->
  glt (order_sum2 r r') (J x C0) (J x' C1).
Proof. 
move=> xsr xsr'; split; last by move => h; move: (pr2_def h); fprops.
apply /orsum2_gleP; split; first by apply: candu2_pra.
  by apply: candu2_prb.
constructor 3; aw; split; fprops.
Qed.

Lemma orprod2_gleP  a b:
  gle (order_prod2 r r') a b <->
  [/\ inc a  (product2 (substrate r') (substrate r)),
     inc b  (product2 (substrate r') (substrate r))&
    ( (Vg a C0 = Vg b C0 /\ gle r (Vg a C1) (Vg b C1)) 
      \/ (glt r' (Vg a C0)(Vg b C0)))].
Proof.
have [wor sr] := cdo_wor.
have la:  orprod_ax canonical_doubleton_order (variantLc r' r).
  by split => //; bw; fprops.
apply: (iff_trans (orprod_gleP la a b)).
have ->: prod_of_substrates (variantLc r' r) =
     (product2 (substrate r') (substrate r)).
  rewrite  - orprod2_sr // /order_prod2;  bw.
rewrite (proj2 cdo_wor).
split; move => [ap2 bp2 h];split => //. 
  case: h.
     move => <-; left;split => //; order_tac. 
     by move: ap2 => / setX2_P [_ _ _]. 
  move=> [j [ /C2_P [] ->]]; bw;first by move => h _; right.
  move=> p1 p2.
  by move: (p2 _ cdo_glt1) => p4; move: p1 => [p1 _]; left.
case: h. 
  move=> [p1 p2]; case: (equal_or_not  (Vg a C1) (Vg b C1)).
    move:ap2 bp2 => /setX2_P [fga da Vaa VBa].
    move => /setX2_P  [fgb db Vab VBb].
    move=> VV; left; apply: fgraph_exten =>//; first by ue. 
    rewrite da; move=> ix xda;try_lvariant xda. 
  move => nVV; right; exists C1; split => //; fprops; bw; first by split.
  move=> i [] /cdo_gleP p3 p4; case: p3; [ | by case | by move=> [-> _]].
  by move=> [r1 r2]; rewrite -r2 in r1. 
move => pa; right; exists C0;bw;split => //; fprops.
move=> i [] /cdo_gleP []; case => // -> -> //.
Qed.

End OrderSum2Basic.

Hint Resolve  orsum2_or orprod2_or: fprops.
Hint Rewrite orsum2_sr orprod2_sr : bw.

Lemma orprod2_totalorder r r':
  total_order r -> total_order r' -> total_order (order_prod2 r r').
Proof.
move: cdo_wor => [ha hb].
move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orprod_total.
  split => //; [ bw | hnf; bw => x xi; try_lvariant xi].
hnf;bw => x xi; try_lvariant xi.
Qed.

Lemma order_prod_pr r r': order r -> order r' ->
 (order_prod2 r r') \Is (order_sum r' (cst_graph (substrate r') r)).
Proof.
move => or or'. 
have oa: (orsum_ax r' (cst_graph (substrate r') r)).
  hnf; split => //; bw; hnf; bw;move=> i isr; bw.
set fo:=order_sum r' (cst_graph (substrate r') r).
have odf: order fo by rewrite /fo; fprops.
move: (orsum_sr oa) => s1.
move: (orprod2_or or odf).
move: (orprod2_sr or or'). 
set io := order_prod2 r r'; move => s2 o2.
pose f x := J (Vg x C1) (Vg x C0).
have ta: (lf_axiom f (substrate io) (substrate  fo)). 
  move=> t; rewrite /fo s1 s2; move /setX2_P => [fgt dt va vb]. 
  apply: disjointU_pi; bw.
have bf: bijection (Lf f (substrate io) (substrate fo)).
  apply: lf_bijective =>//. 
    move=> u v;rewrite s2 /f; move=> ud vd eq.
    move: (pr2_def eq)(pr1_def eq) => p1 p2.
    apply: (setXf_exten ud vd); move=> i itp;  try_lvariant itp.
  rewrite s1 /fam_of_substrates  /cst_graph.
  move=> y ys; move:(du_index_pr1 ys); rewrite Lg_domain.
  move=> [Qsr]; bw; move=> Psr py.
  exists (variantLc (Q y) (P y)).
    rewrite s2; apply /setX2_P;split => //; bw; fprops.
  symmetry;rewrite /f; bw; aw.
exists (Lf f (substrate io) (substrate fo));hnf; split; aw.
    rewrite /io; fprops.
  hnf; split; aw.
hnf; aw; move=> x y xs ys; aw.
move : (ta _ xs) (ta _ ys) => qa qb.
have p1: inc (Vg x C0) (substrate r').
  by  move: xs; rewrite s2; move /setX2_P => [_ _ ].
apply (iff_trans (orprod2_gleP or or' _ _)); rewrite - s2.
symmetry; apply (iff_trans (orsum_gleP _ _ _ _)).
have ->: sum_of_substrates (cst_graph (substrate r') r) = substrate fo by aw.
split; move => [_ _ xx]; split => //; move: xx;
 rewrite /f /order_sum_r  !pr1_pair !pr2_pair; bw; case; fprops.
Qed.

Lemma orsum_total r g:
  orsum_ax r g -> total_order r ->
  (forall i, inc i (domain g) -> total_order (Vg g i)) ->
  total_order (order_sum r g).
Proof. 
move=> oa  [_ tor] alt; rewrite /total_order.
move: (oa) => [or sr alo]; bw. 
rewrite sr in tor.
split =>//; first by fprops.
move=> x y xsr ysr; move: (du_index_pr1 xsr) (du_index_pr1 ysr).
move=> [Qx Px px][Qy Py py].
case: (equal_or_not (Q x) (Q y)). 
  move =>h; move: (alt _ Qx) => [lor ltor]; rewrite -h in Py.
  case: (ltor _ _ Px Py) => h1;aw ; [left | right]; 
    apply /orsum_gleP;split => //; right; split => //; ue.
move=> nQ; case: (tor _ _ Qx Qy) => h; [left | right];
  apply /orsum_gleP;split => //; left;split; fprops.
Qed.

Lemma orsum2_totalorder r r':
  total_order r -> total_order r' -> total_order (order_sum2 r r').
Proof.
have [ha hb] := cdo_wor.
have hc:= (worder_total ha).
have hd := proj1 ha.
move => pa pb; move:(pa)(pb) => [oa _][ob _];  apply: orsum_total => //.
   hnf; split => //; [ bw | hnf; bw => x xi; try_lvariant xi].
hnf;bw => x xi; try_lvariant xi.
Qed.

Lemma orsum_wor r g: 
  worder_on r (domain g) ->  worder_fam g ->
  worder (order_sum r g). 
Proof.
move=> [wor sr] alw; move: (proj1 wor) => or.
have oa: orsum_ax r g by split => // i ie; exact (proj1 (alw _ ie)).
apply:(worder_prop_rev (orsum_or oa)); bw  => x xs [x0 x0x].
set A := fun_image x Q. 
have Asr: (sub A (substrate r)).
  move=> t /funI_P [z zx ->].
  rewrite sr;exact (proj31 (du_index_pr1 (xs _ zx))).
have neA: nonempty A by exists (Q x0); apply /funI_P; ex_tac.
move: (worder_prop wor Asr neA)=> [a aA ale].
set B:= Zo x (fun z => Q z = a).
set C := fun_image B P.
move: (Asr _ aA); rewrite sr => adg.
have Cs: (sub C (substrate (Vg g a))). 
  move=> t /funI_P  [z zB ->].  
  move: zB => /Zo_P [zx] <-; exact (proj32 (du_index_pr1 (xs _ zx))).  
have neC: nonempty C.
  move: aA => /funI_P [z zx qz].
  by exists (P z); apply /funI_P;exists z => //; apply: Zo_i.
move: (worder_prop (alw _ adg) Cs neC)=> [b bC leB].
have Jx: inc (J b a) x.
   move: bC => /funI_P [z /Zo_P [zx <-] ->].
   by rewrite (proj33 (du_index_pr1 (xs _ zx))). 
have ors: order (order_sum r g) by fprops.
ex_tac => c cx.
move: (du_index_pr1 (xs _ cx))=> [Qc Pc pc]. 
apply /orsum_gleP;split; fprops.
hnf; rewrite pr1_pair pr2_pair. 
have QcA:  (inc (Q c) A) by apply /funI_P; ex_tac.
move: (ale _ QcA) => leac.
case: (equal_or_not a (Q c)). 
  move=> aQc; right;split => //.
  have Pcb: (inc (P c) C) by apply/funI_P; exists c => //; apply: Zo_i.
  exact: (leB _ Pcb).
by move => nac; left.
Qed.

End Worder.
Export Worder.