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

Require Export set5.

Set Implicit Arguments.
(* $Id: set6.v,v 1.65 2010/08/02 07:30:56 grimm Exp $ *)

Import Correspondence.
Import Bfunction. 
Import Border.

Module Worder.



(** ** EIII-2-1 Segments of a well-ordered set *)

(** Well ordering *)

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

Definition worder_r r :=
  order_r r & forall x, (forall a, inc a x -> r a a) -> nonempty x ->
    exists y, least_element (graph_on r x) y. 

Lemma wordering_pr: forall r x, worder_r r ->
  (forall a, inc a x -> r a a)  ->  
  (substrate (graph_on r x) = x & worder (graph_on r x)).
Proof. ir. assert (substrate (graph_on r x) = x).  
  rww substrate_graph_on. split. ee. am. nin H.
  assert (Ha: order (graph_on r x)). app order_from_rel. 
  split. am. rw H1. ir.
  assert  (forall a, inc a x0 -> r a a). ir. set (H3 _ H5). wri H1 i.
  assert (related (graph_on r x) a a). order_tac. rwi graph_on_rw1 H6.  eee.
  nin (H2 _ H5 H4). exists x1. red in H6. rwii substrate_graph_on H6. ee.
  red. aw. split. am. ir. set (H7 _ H8).  rwi graph_on_rw1 g.
  aw. rww graph_on_rw1. eee. ue.
Qed.


Lemma singleton_emptyset_not_empty: (singleton emptyset) <> emptyset.
Proof. red. ir. assert (inc emptyset (singleton emptyset)). fprops. rwi H H0.
  elim (emptyset_pr H0).
Qed.

Hint Resolve singleton_emptyset_not_empty two_points_distinctb: fprops.

(** We sometimes need an ordered set with two elements *)

Definition canonical_doubleton_order :=
  union2 (doubleton (J TPa  TPa) (J TPb TPb)) (singleton (J TPa TPb)).

Lemma canonical_doubleton_order_pr: forall x y,
  gle canonical_doubleton_order x y =
  ( (x= TPa & y = TPa) \/  (x= TPb & y = TPb) \/  (x= TPa & y = TPb)).
Proof. ir. uf gle. uf related. uf canonical_doubleton_order. app iff_eq. ir. 
  nin (union2_or H). nin (doubleton_or H0). left. ee; inter2tac.
  right. left. ee; inter2tac.
  cp (singleton_eq H0). right. right. ee; inter2tac. 
  ir. nin H;  [ | nin H ];ee;  rw H; rw H0. app union2_first. fprops. 
  app union2_first. fprops.  app union2_second. fprops.
Qed.

Lemma substrate_canonical_doubleton_order:
  substrate canonical_doubleton_order = two_points.
Proof. assert (Ha:is_graph canonical_doubleton_order). red. 
  uf canonical_doubleton_order. ir. nin (union2_or H).
  nin (doubleton_or H0); rw H1; fprops. db_tac.
  set_extens. rwi (inc_substrate_rw x Ha) H. nin H. nin H.
  cp (canonical_doubleton_order_pr x x0). ufi gle H0. ufi related H0. rwi H0 H.
  nin H. ee. rw H. uf TPa. app R_inc. nin H. ee. rw H. uf TPb; ap R_inc.
  ee; rw H. uf TPa. ap R_inc. nin H. cp (canonical_doubleton_order_pr x0 x).  
  ufi gle H0. ufi related H0. rwi H0 H. nin H. ee. rw H1. uf TPa; ap R_inc.
  nin H. ee. rw H1. uf TPb;  ap R_inc. ee; rw H1. uf TPb; ap R_inc. 
  rwi two_points_pr H.
  nin H; assert (related canonical_doubleton_order x x);
  try rw canonical_doubleton_order_pr. left. eee. substr_tac. rw H. au.
  substr_tac.
Qed.

Lemma worder_canonical_doubleton_order: worder canonical_doubleton_order.
Proof. assert (He:=  substrate_canonical_doubleton_order).
 assert (Ha:is_graph canonical_doubleton_order). red. 
  uf canonical_doubleton_order. ir. nin (union2_or H).
  nin (doubleton_or H0); rw H1; fprops. db_tac.   
  assert (order canonical_doubleton_order). 
  red;  ee; red; split; tv; ir ; rewrite canonical_doubleton_order_pr in *.
  ir. rwi He H. rwi two_points_pr H. 
  nin H. left. eee. right. left. eee. 
  ir. nin H. nin H. wri H1 H. rww H. nin H. nin H. wri H1 H. rww H. nin H0.
  left. intuition. right. right. nin H0; intuition. 
  ir. nin H ; [ |  nin H ]; ee; try ( solve [ ue]);
  nin H0 ; [ | nin H0]; ee;  ue.
  split. am. ir. rwi He H0.
  nin (inc_or_not TPa x). ir. 
  exists TPa. red. aw. ee. am. ir. aw. rw canonical_doubleton_order_pr.
  cp (H0 _ H3).  rwi two_points_pr H4. nin H4. rw H4. intuition. 
  rw H4. intuition. rww He. ir.
  nin H1. exists y. red.  aw. ee. am. ir. aw. rw canonical_doubleton_order_pr.
  cp (H0 _ H3). rwi two_points_pr H4. nin H4. wri H4 H2.
  elim H2. am. rw H4. cp (H0 _ H1).  rwi two_points_pr H5. nin H5; au.
  rww He.
Qed.

(** A well ordering is total; bounded sets have a supremum *)

Lemma worder_total: forall r, worder r -> total_order r.
Proof. ir. red. ir. nin H. split. am. ir. set (u:=doubleton x y).
  assert (sub u (substrate r)). uf u. app sub_doubleton. assert (nonempty u).
  uf u. app nonempty_doubleton. nin (H0 _ H3 H4). red in H5.
  ee. awii H5.  awii H6. ufi u H5. 
  assert (inc y u). uf u. fprops.  assert (inc x u). uf u. fprops. 
  nin (doubleton_or H5); wr H9 ;
  [left;   set (H6 _ H7) | right; set (H6 _ H8) ] ;
  app (related_induced_order1 g). 
Qed.

Lemma worder_hassup: forall r A, worder r -> sub A (substrate r) ->
  bounded_above r A -> has_supremum r A.
Proof. ir. red in H. red in H1. nin H1. red. uf least_upper_bound.
  set (X:= (Zo (substrate r) (fun z  => upper_bound r A z))).
  assert (sub X (substrate r)). uf X. app Z_sub. assert (nonempty X).
  uf X. exists x. Ztac. red in H1. ee. am. ee. ap (H4 _ H2 H3). 
Qed.

Lemma induced_trans: forall r x y,
  order r -> sub x y-> sub y (substrate r) ->
  induced_order r x = induced_order (induced_order r y) x.
Proof. ir. uf induced_order. 
  set_extens; nin (intersection2_both H2); inter2tac.
  inter2tac. uf coarse. ufi coarse H4. awi H4. ee. 
  app product_inc; app H0. inter2tac.
Qed.

Lemma worder_restriction: forall r A, worder r -> sub A (substrate r) ->
  worder (induced_order r A).
Proof. ir. red in H. ee. red. split. fprops. ir. awii H2.
  wr (induced_trans H H2 H0). app H1. apw sub_trans  A. 
Qed.

Lemma worder_least: forall r, worder r -> nonempty (substrate  r) ->
  exists y, least_element r y.
Proof. ir.  red in H. ee. nin (H1 _ (@sub_refl (substrate r)) H0).
  rwi induced_order_substrate H2. exists x. am. am.
Qed.

(** A set remains well-ordered after adjoining a greatest element *)
  
Lemma singleton_pr1: forall a x, nonempty x ->
  (forall z, inc z x -> z = a) -> x = singleton a.
Proof.  ir. rww singleton_pr. split.  nin H. wrr (H0 _ H). am.
Qed.

Lemma worder_adjoin_greatest: forall r a, worder r-> ~ (inc a (substrate r))
  -> worder (order_with_greatest r a).
Proof. ir. red in H. ee. set (order_with_greatest_pr H H0). ee. 
  split. am. rw H3. ir. set (y := intersection2 x (substrate r)).
  nin (emptyset_dichot y).
  assert (x = singleton a). app singleton_pr1. ir. set (H6 _ H9).
    rwi tack_on_inc i. nin i. empty_tac1 z.
    uf y. inter2tac. am. 
  exists a. red. aw. rw H9. split. fprops. ir. aw. awi H10.
  uf order_with_greatest. red. red. app union2_second. rw H10. 
  app product_pair_inc; fprops. db_tac. ue.
  assert (sub y (substrate r)). uf y. app intersection2sub_second.
  nin (H1 _ H9 H8). exists x0. red in H10.  awi H10. nin H10. red. aw.  split.
  ufi y H10. inter2tac. assert (inc x0 x). ufi y H10. inter2tac.
  ir. cp (H6 _ H13). rwi tack_on_inc H14. aw. red. red. uf order_with_greatest. 
  nin H14. assert (inc x1 y). uf y. inter2tac. cp (H11 _ H15).
  cp (related_induced_order1 H16).  red in H17. red in H17. inter2tac. 
  app union2_second. rw H14. app product_pair_inc. app H6. fprops. ue. 
  am. am. 
Qed.

Lemma inc_lt1_substrate: forall r x y, glt r x y -> inc x (substrate r).
Proof. ir. order_tac.  Qed.

Lemma inc_lt2_substrate: forall r x y, glt r x y -> inc y (substrate r).
Proof. ir. order_tac. Qed.

Lemma not_lt_self: forall r x, glt r x x -> False.
Proof. ir. nin H. elim H0. tv. Qed.

(** Two stricly increasing functions with the same range are equal if the source is well-ordered *)
Lemma strict_increasing_extens: forall 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. ir. set (A:=Zo (source f)(fun x=> W x f <> W x g)). red in H; red in H0.
  assert (Ha: total_order r). app worder_total.
  ee. nin (emptyset_dichot A). app function_exten. ue. ue. 
  ir. ex_middle.  empty_tac1 x.
  uf A. Ztac. nin H1. assert (sub A (source f)). uf A. app Z_sub. 
  rwi H10 H14. nin (H14 _ H15 H13). red in H16. awi H16. 
  nin H16. assert (Hb: inc x (source f)). app H15.
  assert (inc (W x f) (range (graph g))). wr H2. app inc_W_range_graph.
  rwii range_inc_rw H18. nin H18. nin H18.
  assert (inc (W x g) (range (graph f))). rw H2. app inc_W_range_graph.
  wr H5. rww H10. rwii range_inc_rw H20. nin H20. nin H20.
  assert (glt r' (W x g) (W x f)). assert (glt r x x0).  red in Ha. ee.
  assert (x <> x0).  red. ir.  wri H24 H19. ufi A H16. Ztac. contradiction.
  assert (inc x (substrate r)). ue. 
  assert (inc x0 (substrate r)). ue. nin (H23 _ _ H25 H26). split; am.
  assert (glt r x0 x).  red in H27. red. ee. am. intuition. 
  cp (H12 _ _ H28). assert (inc x0 A). uf A. Ztac. wrr H10.
  nin H29. ue.  cp (H17 _ H30). split. ap (related_induced_order1 H31). am.
  rw H19. app H7. 
  assert (glt r' (W x f) (W x g) ). assert (glt r x x1).  red in Ha. ee.
  assert (x <> x1).  red. ir. wri H25 H21. ufi A H16. Ztac. elim H27. sy. am.
  wri H10 Hb. wri H10 H20. nin (H24 _ _ Hb H20). split;am.
  assert (glt r x1 x). red in H26. red. ee. am. intuition. 
  cp (H7 _ _  H27). assert (inc x1 A). uf A. Ztac. ue. nin H28. 
  wr H21. dneg. sy; am. cp (H17 _ H29). split. 
  ap (related_induced_order1 H30). am. rw H21. app H12.
  order_tac. am. rww H10.
Qed.


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

Definition is_segment 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 segment_c r s := interval_uc r s.

Lemma lt_in_segment: forall r s x y,
  is_segment r s ->  inc x s -> glt r y x -> inc y s.
Proof. ir. red in H; red in H1;  ee. app (H3 _ _ H0 H1).
Qed.

Lemma inc_segment: forall r x y,
  inc y (segment r x) -> glt r y x.
Proof. ir. ufi segment H. ufi interval_uo H. Ztac. am.
Qed.

Lemma not_in_segment : forall r x,  inc x (segment r x) -> False.
Proof. ir. set (inc_segment H).  elim (not_lt_self g). Qed.

Lemma sub_segment: forall r x, sub (segment r x) (substrate r).
Proof. ir. red. ir. ufi segment H. ufi interval_uo H. Ztac. am.
Qed.

Lemma sub_segment1: forall r s,  is_segment r s -> sub s (substrate r).
Proof. ir. red. ir. red in H. eee. 
Qed.

Lemma sub_segment2: forall r x y,
  sub (segment (induced_order r x) y) x.
Proof. ir. red. uf segment. uf interval_uo.  ir. Ztac. red in H1. ee.
  red in H1. red in H1. ufi induced_order H1. set (intersection2_second H1).
  ufi coarse i. awi i. eee. 
Qed.

Lemma segment_inc: forall r x y, inc x (substrate r) ->
  glt r y x -> inc y (segment r x). 
Proof. ir. uf segment. uf interval_uo. Ztac. order_tac.
Qed.

Lemma segment_rw: forall r x y, inc x (substrate r) ->
  inc y (segment r x) = glt r y x.
Proof. ir. app iff_eq.  ir. app inc_segment.  ir. app segment_inc. 
Qed.

Lemma segmentc_rw: forall r x y, inc x (substrate r) ->
  inc y (segment_c r x) = gle r y x.
Proof. ir. uf segment_c. uf interval_uc. app iff_eq.  ir.  Ztac. am. ir.
  Ztac. order_tac.
Qed.

Lemma inc_bound_segmentc: forall r x, order r -> inc x (substrate r) ->
  inc x (segment_c r x).
Proof. ir. rww segmentc_rw. order_tac.
Qed.

Lemma sub_segmentc: forall r x, sub (segment_c r x) (substrate r).
Proof. ir. red. ir. ufi segment_c H. ufi interval_uc H. Ztac. am.
Qed.

Hint Resolve inc_bound_segmentc: fprops.


Lemma segment_c_pr: forall r x, order r -> inc x (substrate r) ->
  tack_on (segment r x) x = segment_c r x.
Proof. ir. uf segment_c. uf interval_uc. set_extens.
  rwi tack_on_inc H1. nin H1.  Ztac. app (sub_segment H1).  
  cp (inc_segment H1). fprops. order_tac. Ztac. rww H1. rww H1. order_tac.
  Ztac. nin (equal_or_not x0 x).
  rw H4. fprops. rw tack_on_inc. left. app segment_inc. red. au. 
Qed.

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

Lemma empty_is_segment: forall r, is_segment r emptyset.
Proof. ir. red. split. ap emptyset_sub_any. ir. elim (emptyset_pr H). Qed.

Lemma substrate_is_segment: forall r, order r -> is_segment r (substrate r).
Proof. ir. red. eee. ir. order_tac.  Qed.

Lemma subsegment_is_segment: forall r s s', order r -> 
  is_segment r s -> is_segment (induced_order r s) s' -> is_segment r s'.
Proof. ir. cp (sub_segment1 H0). red. red in H1. ee. awi H1. 
  app (sub_trans (a:=s')(b:=s)). am. am. ir. awi H1. cp (H1 _ H4).
  red in H0. ee. cp (H7 _ _ H6 H5).  cp (H3 x y H4). awi H9. app H9. am. am.
  am. am.
Qed.

Lemma intersection_is_segment: forall r s , order r -> nonempty s ->
  (forall x, inc x s -> is_segment r x) -> is_segment r (intersection s).
Proof. ir. red. split. nin H0. nin (H1 _ H0). red. ir.
  ap (H2 _ (intersection_forall H4 H0)). ir. app intersection_inc. ir.
  nin (H1 _ H4). ap (H6 _ _ (intersection_forall H2 H4) H3).
Qed.

Lemma unionf_is_segment: forall r j s, order r -> 
  (forall x, inc x j -> is_segment r (s x)) -> is_segment r (unionf j  s).
Proof. ir. red. split. red. ir. nin (unionf_exists H1). nin H2.
  nin (H0 _ H2). app H4. ir. nin (unionf_exists H1).  nin H3. union_tac.
  nin (H0 _ H3). ap (H6 _ _ H4 H2). 
Qed.

Lemma union_is_segment: forall r s , order r -> 
  (forall x, inc x s -> is_segment r x) -> is_segment r (union s).
Proof. ir. red. split. red. ir. nin (union_exists H1).   nin H2.
  nin (H0 _ H3). app H4. ir.  nin (union_exists H1).  nin H3. 
  nin (H0 _ H4). apply union_inc with x0. ap (H6 _ _ H3 H2). am.
Qed.

Lemma segment_is_segment: forall r x, order r -> 
  inc x (substrate r) -> is_segment r (segment r x).
Proof. ir. uf segment. red. uf interval_uo. split. app Z_sub. ir. Ztac.
  clear H1. Ztac. order_tac. order_tac. 
Qed.

Theorem well_ordered_segment: forall r s, worder r -> is_segment r s ->
  s = substrate r \/ (exists x, inc x (substrate r) & s = segment r x).
Proof. ir. nin(equal_or_not s (substrate r)).  au. right.
  set (y:= complement (substrate r) s).  assert (nonempty y).
  nin H0. uf y. app strict_sub_nonempty_complement. split; am. 
  clear H1. cp (worder_total H). 
  assert (sub y (substrate r)). uf y. app sub_complement.
  red in H. ee. nin (H4 _ H3 H2). exists x. red in H5. awii H5. nin H5. 
  assert (inc x (substrate r)). app H3. split. am.  
  set_extens. assert (inc x0 (substrate r)). app (sub_segment1 H0). 
  rw segment_rw. awi H5. nin (total_order_pr2 H1 H9 H7). am. 
  red in H0. ee. cp  (H11 _ _ H8 H10). ufi y H5. srwi H5. 
  nin H5. contradiction. am. ex_middle.
  assert (inc x0 y). uf y.  srw. ee. app (sub_segment H8). am.
  cp (H6 _ H10). cp (related_induced_order1 H11). cp (inc_segment H8). 
  order_tac. 
Qed.

Lemma segment_alt: forall r x a, order r -> least_element r a ->
  segment r x = interval_co r a x.
Proof. ir. uf segment. uf interval_co. uf interval_uo. set_extens. red in H0.
  ee. Ztac. Ztac. ee.  am.
Qed.

Lemma segment_alt1: forall r s, worder r -> is_segment r s ->
  s = substrate r \/ (exists x, exists a, s = interval_co  r a x).
Proof. ir. nin (emptyset_dichot (substrate r)). left. red in H0. ee.
  rwi H1 H0. rw H1. ap extensionality. am. app emptyset_sub_any.
  nin (well_ordered_segment H H0). au. nin H2. right.
  nin (worder_least H H1).  cp H3. nin H3. exists  x. exists x0. nin H2.
  rw H6. app segment_alt. nin H; am. 
Qed.

Lemma segment_monotone: forall r x y, order r -> gle r x y ->
  sub (segment r x)  (segment r y).
Proof. ir. red. ir. cp (inc_segment H1). app segment_inc. order_tac.
  order_tac.
Qed.

Lemma segment_dichot_sub: forall r x y,
  worder r -> is_segment r x -> is_segment r y ->
  (sub x y \/ sub y x).
Proof. ir. nin (well_ordered_segment H H0). rw H2. right.
  app sub_segment1. nin H2. ee. nin (well_ordered_segment H H1). 
  rw H4. left. app sub_segment1. nin H4. ee. cp (worder_total H).
  red in H6. ee. rw H3; rw H5. 
  nin (H7 _ _ H2 H4); [ left | right];  app segment_monotone.
Qed.

Lemma le_in_segment: forall 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. ir. app segment_inc. set (inc_segment H1). order_tac.
Qed. 
  
Lemma coarse_segment_monotone: forall r x y, order r -> gle r x y ->
  sub (coarse (segment r x)) (coarse (segment r y)).
Proof. ir. cp (segment_monotone H H0). uf coarse.
  app product_monotone.
Qed.

Lemma segment_induced_a: forall r s x,
  order r -> is_segment r s -> inc x s -> 
  segment (induced_order r s) x = segment r x.
Proof. ir. set_extens.  cp (inc_segment H2). cp (related_induced_order2 H3). 
  app segment_inc. order_tac. app segment_inc. aw. 
  red in H; eee. app sub_segment1. cp (inc_segment H2). red in H3. ee.
  red. ee. aw. red in H0. ee. app (H5 _ _ H1 H3). am.
Qed.  

Lemma tack_on_segment: forall r x,
   order r -> inc  x (substrate r) ->
  is_segment r (segment_c r x).
Proof. ir. red.  uf segment_c. uf interval_uc. ee.  app Z_sub. ir.
  Ztac. clear H1. Ztac. order_tac.  order_tac. 
Qed.

Lemma segment_induced: forall r x x0, order r ->  glt r x0 x ->
  segment (induced_order r (segment r x)) x0 = segment r x0.
Proof. ir.  cp (inc_lt2_substrate H0). rww segment_induced_a. 
  app segment_is_segment. rww segment_rw.  
Qed.
  
Lemma segment_induced1: forall r x x0, order r ->  glt r x0 x ->
  segment (induced_order r (segment_c r x)) x0 = segment r x0.
Proof. ir. cp (inc_lt2_substrate H0). rww segment_induced_a.  
  app tack_on_segment. wrr segment_c_pr. 
  rw tack_on_inc. left. rww segment_rw.
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 *)

Lemma union_segments: forall r, total_order r ->
  let E := substrate r in 
    let A := union (fun_image E (fun x => (segment r x))) in
      ( (forall x, ~ (greatest_element r x)) -> A = E)
      & (forall x, greatest_element r x -> A = complement E (singleton x)).
Proof. ir. assert (forall x, inc x A = exists y, glt r x y). ir. uf A. 
  app iff_eq. ir. nin (union_exists H0). nin H1. awi H2. nin H2. nin H2.
  wri H3 H1. exists x1. app inc_segment. 
  ir. nin H0. assert (inc x0 E). uf E. order_tac.
  apw union_inc (segment r x0). app segment_inc. aw. ex_tac. 
  assert (sub A E). red. ir. rwi H0 H1. nin H1. uf E. order_tac. 
  split; ir; set_extens. ir. rw H0. app exists_proof. red; ir. elim (H2 x). 
  split. am. ir. nin (total_order_pr2 H H3 H5). elim (H4 x0). am. am.
  srw. split. app H1. aw. red. ir. rwi H4 H3. nin H2. rwi H0 H3. nin H3. 
  cp (H5 _  (inc_lt2_substrate H3)). nin H. order_tac.
  srwi H3. ee. awi H4. rw H0. exists x. nin H2. split. app H5. am.
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 set_of_segments_strict r:= 
  fun_image (substrate r) (fun x => (segment r x)).
Definition set_of_segments r:= 
  tack_on (set_of_segments_strict r) (substrate r).
Definition  set_of_segments_iso r:= 
  BL(segment r) (substrate r) (set_of_segments_strict r).

Lemma inc_set_of_segments: forall r x, worder r ->
  is_segment r x = inc x (set_of_segments r).
Proof. ir. app iff_eq.  ir. cp (well_ordered_segment H H0).
  uf set_of_segments. nin H1. rw H1. fprops. rw tack_on_inc. left.
  uf set_of_segments_strict. aw. nin H1. exists x0.  intuition.
  ir. ufi set_of_segments H0. rwi tack_on_inc H0. nin H0. 
  ufi set_of_segments_strict H0. awi H0. nin H0. nin H0.
  wr H1. app  segment_is_segment.  red in H. ee. am. rw H0. red.
  split. fprops. ir. order_tac.
Qed.

Lemma sub_set_of_segments: forall r x, worder r ->
  inc x (set_of_segments r) -> sub x (substrate r).
Proof. ir. wri inc_set_of_segments H0.  red in H0. nin H0. am. am.
Qed.

Lemma set_of_segments_axiom: forall r, worder r ->
  transf_axioms (segment r) (substrate r) (set_of_segments_strict r).
Proof. ir. red. ir. uf set_of_segments_strict. aw. ex_tac. 
Qed.

Lemma segment_injective: forall r x y, total_order r ->
  inc x (substrate r) ->  inc y (substrate r) -> segment r x = segment r y ->
  x = y.
Proof. ir.
  nin (total_order_pr1 H H0 H1); try rwi ggt_invb H3; wrii segment_rw H3.
  wri H2 H3. elim (not_in_segment H3).
  rwi H2 H3. nin H3. elim (not_in_segment H3). am. 
Qed.

Lemma segment_injective1: forall r x y, worder r ->
  inc x (substrate r) ->  inc y (substrate r) -> segment r x = segment r y ->
  x = y.
Proof.  ir. app (segment_injective (worder_total H) H0 H1 H2).
Qed.

Lemma set_of_segments_iso_bijective:forall r, worder r ->
  bijective (set_of_segments_iso r).
Proof. ir. uf set_of_segments_iso.  app bl_bijective.
  app set_of_segments_axiom. ir. app (segment_injective1 H H0 H1 H2). 
  ir. ufi set_of_segments_strict H0. awi H0. nin H0. nin H0. ex_tac. 
Qed.

Theorem set_of_segments_iso_isomorphism:forall r, worder r ->
  order_isomorphism (set_of_segments_iso r) r 
  (inclusion_suborder (set_of_segments_strict r)).
Proof. ir. assert (Ha:= set_of_segments_axiom H). cp H. red in H. red.
  uf set_of_segments_iso. aw. eee. ap (set_of_segments_iso_bijective H0). 
  ir. aw. app iff_eq. ir. eee. app segment_monotone. ir. ee.
  nin (total_order_pr2  (worder_total H0) H3 H2).
  wri segment_rw H7. cp (H6 _ H7). elim (not_in_segment H8). am. am.
Qed.

Theorem set_of_segments_worder:forall r, worder r ->
  worder (inclusion_suborder (set_of_segments r)).
Proof. ir. cp H. cp (worder_total H0).  
  assert (order (inclusion_suborder (set_of_segments r))). fprops. 
  red. split. am. aw. ir. 
  set (y := intersection2 x (set_of_segments_strict r)).
  nin (emptyset_dichot y). uf set_of_segments.
  assert (x = singleton (substrate r)). app singleton_pr1.
  ir. ufi set_of_segments H3. cp (H3 _ H6). rwi tack_on_inc H7. nin H7. 
  empty_tac1 z. uf y. inter2tac. am.  rw H6.
  exists (substrate r). red. aw. eee. ir. awi H7. rw H7. aw. fprops. red. 
  ir.  awi H7.  rw H7. fprops.
  assert (sub y (set_of_segments_strict r)). uf y. app intersection2sub_second.
  assert (forall a, inc a y -> exists u, 
    inc u (substrate r) &  segment r u = a).
  ir. cp (H6 _ H7). ufi set_of_segments_strict  H8. awi H8. am.
  set (cf := fun a=> choose (fun u => inc u (substrate r) & segment r u = a)).
  assert (forall a, inc a y -> 
     (inc (cf a) (substrate r) & segment r (cf a) = a)).
  ir.  uf cf. app choose_pr. app H7.
  set (z:= fun_image y cf). 
  assert (nonempty z). nin H5. exists (cf y0). uf z. aw. ex_tac.
  assert (sub z (substrate r)). red. ir. ufi z H10. awi H10. nin H10. nin H10.
  wr H11. cp (H8 _ H10). nin H12; am.
  red in H. ee. nin (H11 _ H10 H9).  exists (segment r x0). red. aw. split.
  assert (inc x0 z). red in H12. ee. awi H12. am. am. am.
  assert (inc (segment r x0) y). ufi z H13. awi H13. nin H13.
  assert (segment r x0 = x1). nin H13. cp (H8 _ H13). eee. 
  rw H14. nin H13. am. ufi y H14. inter2tac. 
  ir. red in H12. ee. awi H12.
  assert (Ha:inc (segment r x0) x). assert (inc (segment r x0) y). ufi z H12. 
  awi H12. nin H12. nin H12. wr H15. cp (H8 _ H12). eee. 
  ufi y H15. inter2tac.
  nin (inc_or_not x1 y). ir. 
  assert (inc (cf x1) z). uf z. aw. ex_tac. awi H14.
  cp (H14 _ H16). awi H17. aw. ee. uf set_of_segments. rw tack_on_inc. left. 
  uf set_of_segments_strict. aw. cp (H10 _ H12). ex_tac.
  uf set_of_segments. rw tack_on_inc. left. 
  app H6. cp (H8 _ H15). ee. wr H19. red. ir. rwi segment_rw H20. 
  app segment_inc. order_tac. app H10. am. am. am. am.
  assert (x1 = substrate r). cp (H3 _ H13). ufi set_of_segments  H16.
  rwi tack_on_inc  H16. nin H16. elim H15. uf y. inter2tac. am.
  aw. split. uf set_of_segments. rw tack_on_inc. left. 
  uf set_of_segments_strict. aw. exists x0. split.  app H10. tv. split.
  uf set_of_segments. fprops. rw H16. app sub_segment.  am. am.
Qed.


(** We consider a property A(g) that says that g is a family of orders indexed 
by I, such that if the substrate of g(i) is a subset of the substrate of g(j)
then both ordering coincides on g(i). Moreover, for every i, j there is k such 
that the substrate of g(k) is a subset of the substrates of g(i) and g(j).
We consider B(g,h), that says that h is an ordering on the union of the 
substrates, compatible with g. There is a unique h, the union of g.  *)
Definition common_extension_order g h:=
  order h & substrate h = unionf (domain g) (fun a =>  (substrate (V a g))) &
  (forall a, inc a (domain g) -> V a g = induced_order h (substrate (V a g))).

Definition common_extension_order_axiom g :=
  fgraph g &
  (forall x, inc x (domain g) -> order (V x g)) &
  (forall a b, inc a (domain g) -> inc b (domain g )-> exists c, 
    inc c (domain g) & sub (substrate (V a g)) (substrate (V c g))
    & sub (substrate (V b g)) (substrate (V c g))) &
  (forall a b, inc a (domain g) -> inc b (domain g) ->
    sub (substrate (V a g)) (substrate (V b g)) ->
    V a g = induced_order (V b g) (substrate (V a g))).


Lemma order_merge1: forall g, 
  common_extension_order_axiom g -> common_extension_order g (unionb g).
Proof. ir. red in H. ee. assert (is_graph (unionb g)). red. ir. 
  nin (unionb_exists H3). nin H4.  cp (H0 _ H4).  nin H6. nin H6. app H6.
  set (E:=unionf (domain g) (fun a : Set => substrate (V a g))). 
  assert (Ha:forall y,inc y E ->  related (unionb g) y y). 
  ir. ufi E H4. nin (unionf_exists H4). nin H5.
  red. union_tac. set (H0 _ H5).  order_tac. 
  assert (substrate (unionb g)= E). set_extens. rwi inc_substrate_rw H4. 
  nin H4;  nin H4; nin (unionb_exists H4); nin H5; cp (H0 _ H5);
  uf E; union_tac; substr_tac. am.
  cp (Ha _ H4).  substr_tac.
  assert (forall x y, inc x (unionb g) -> inc y (unionb g) -> 
    exists u, inc u (domain g) & inc x (V u g) & inc y (V u g)).
  ir. nin (unionb_exists H5). nin (unionb_exists H6). ee. 
  cp (H1 _ _ H7 H8). nin H11. ee. exists x2. split. am.
  cp (H2 _ _ H7 H11 H12). cp (H2 _ _ H8 H11 H13).
  ufi induced_order H14. ufi induced_order H15.
  split. rwi H14 H10.  inter2tac. rwi H15 H9. inter2tac.
  red. ee. red. ee.  red. eee. red. eee. ir.
  red in H6; red in H7. nin (H5 _ _ H6 H7).  ee. cp (H0 _ H8). 
  red.  union_tac. order_tac.
  red. ir. split. am.  ir. nin (H5 _ _ H6 H7).  ee. cp (H0 _ H8). 
  app (order_antisymmetry H11 H9 H10). am.
  ir.  uf induced_order. set_extens. inter2tac.
  union_tac. cp (H0 _ H6).  nin H8; nin H8.
  cp (sub_graph_coarse_substrate H8). app H11.
  cp (intersection2_first H7). cp (unionb_exists H8). nin H9.
  ee. nin (H1 _ _ H6 H9). ee. cp (H2 _ _ H6 H11 H12).
  cp (H2 _ _ H9 H11 H13). rw H14. uf induced_order.
  rwi H15 H10.  ufi induced_order H10. inter2tac; inter2tac.
Qed.


Lemma order_merge2: forall g h1 h2,  common_extension_order_axiom g -> 
  common_extension_order g h1 ->
  common_extension_order g h2 -> (h1 = h2).
Proof. ir.
  assert (forall h1 h2, common_extension_order g h1 ->
  common_extension_order g h2 -> sub h1 h2).
  ir. red in H. red in H2. red in H3. ee. red. ir.
  assert (J (P x) (Q x) = x). aw.  nin H2; nin H2; app H2.
  assert (inc (P x) (substrate h0)).  substr_tac.
  assert (inc (Q x) (substrate h0)).  substr_tac.
  rwi H6 H14. rwi H6 H13. nin (unionf_exists H13). nin (unionf_exists H14).
  ee. nin (H9 _ _ H15 H16). ee. cp (H7 _ H19). cp  (H5 _ H19). 
  ufi induced_order H22.  ufi induced_order H23. 
  assert (inc x (V x2 g)). rw H22. inter2tac. uf coarse. 
  wr H12. fprops. rwi H23 H24. inter2tac.
  app extensionality; app H2.
Qed.

(** A variant of the previous definition. We assume that the substrates s(i)
and s(j) of g(i) or g(j) are segments one of the other; moreover g(i) is 
well-ordered. There exists a unique h, as above, with additional properties.
*)

Definition common_worder_axiom g:=
  fgraph g &       
  (forall x, inc x (domain g) -> worder (V x g)) &
  (forall a b, inc a (domain g) -> inc b (domain g) -> 
    is_segment (V a g) (substrate (V b g))
    \/ is_segment (V b g) (substrate (V a g))) & 
  (forall a b, inc a (domain g) -> inc b (domain g) ->
    sub (substrate (V a g)) (substrate (V b g)) ->
    V a g = induced_order (V b g) (substrate (V a g))).

Lemma order_merge3: forall g,
  common_worder_axiom g -> common_extension_order_axiom g.
Proof. ir. red in H. red. eee. ir. cp (H0 _ H3).  nin H4; am.
  ir. nin (H1 _ _ H3 H4). red in H5. ee. clear H4. ex_tac. eee.
  red in H5. ee. clear H3. ex_tac. eee. 
Qed.

Lemma order_merge4: forall g, 
  common_worder_axiom g -> common_extension_order g (unionb g).
Proof. ir.  app order_merge1.  app order_merge3. Qed.

Lemma order_merge5: forall g h1 h2,  common_worder_axiom g -> 
  common_extension_order g h1 ->
  common_extension_order g h2 -> (h1 = h2).
Proof. ir. cp(order_merge3 H). app (order_merge2 H2 H0 H1). Qed.

Theorem worder_merge: forall g, common_worder_axiom g ->
 ( (common_extension_order g (unionb g)) &
   worder (unionb g) &
   (forall a x, inc a (domain g) -> is_segment (V a g) x 
     -> is_segment (unionb g) x ) &
   (forall a x, inc a (domain g) ->  inc x (substrate (V a g)) ->
     segment (V a g) x = segment (unionb g) x) &
   (forall x, is_segment (unionb g) x ->
     x = substrate (unionb g) \/ 
       exists a,  inc a (domain g) & is_segment (V a g) x)).
Proof. ir. cp (order_merge4 H). split. am. red in H0.  nin H0. nin H1.
  assert (forall a, inc a (domain g) -> 
      sub (substrate (V a g)) (substrate (unionb g))).
  ir. rw H1. red. ir. apply unionf_inc with a. am. am.
  assert (forall a, inc a (domain g) ->
      is_segment (unionb g) (substrate(V a g))).
  ir. red.  ee. app H3. ir.
  assert (inc y (substrate  (unionb g))). order_tac. red in H6. red in H6.
  nin (unionf_exists H6). ee.
  red in H. ee. nin (H11 _ _ H4 H8).  red in H13. ee. app H13. substr_tac.
  nin H13. app (H14 _ _ H5 H9).
  assert (forall a x, inc a (domain g) -> inc x (substrate (V a g)) 
    -> segment (V a g) x = segment (unionb g) x).
  ir. set_extens. cp (inc_segment H7). red in H8. rw segment_rw. red. ee.
  red. red. apply unionb_inc with a. am. exact H8. am. app (H3 _ H5).
  cp (inc_segment H7). red in H8. rw segment_rw. red. ee.
  red in H8. red in H8. nin (unionf_exists H8).  ee.  
  assert(inc x0 (substrate (V a g))). red in H. ee. nin (H13 _ _ H5 H10). 
  red in H15. ee. app H15. substr_tac. nin H15. app (H16 _ _ H6 H11).
   rw H2. aw.  am. am. am.
  assert (forall a x, inc a (domain g) -> is_segment (V a g) x -> 
    is_segment (unionb g) x).
  ir. red in H. ee. cp (H8 _ H6). cp (well_ordered_segment H11 H7).
  nin H12. rw H12. app H4. nin H12. nin H12. rw H13. rw H5.
  app segment_is_segment. rw H1. apply unionf_inc with a. am. am. am. am.
  assert (worder (unionb g)). red. split. am. ir. nin H8. 
  cp (H7 _ H8). rwi H1 H9. nin (unionf_exists H9). nin H10.
  set (x1:= intersection2 x (substrate (V x0 g))).
  assert (sub x1 (substrate (V x0 g))). uf x1. ap intersection2sub_second.
  assert (nonempty x1). uf x1. exists y. inter2tac. red in H. ee.
  cp (H14 _ H10).  nin H17. ee. cp (H18 _ H12 H13). nin H19. exists x2.
  red in H19. red. ee. awi H19. aw. ufi x1 H19. inter2tac.
  am. am. ir. awii H21. awii H19. clear H18. cp (H7 _ H21). rwi H1 H18.
  nin (unionf_exists H18). nin H22. aw. nin (H15 _ _ H10 H22).
  red in H24. nin H24. awi H20.
  assert (inc x3 (substrate (V x0 g))). app H24.
  assert (inc x3 x1). uf x1. inter2tac. cp (H20 _ H27). awi H28.
  rwi H2 H28.  awi H28. am. ap H12. am. am. am. am. am. am. am.
  awi H20. red in H24. nin H24.
  assert (inc x2 (substrate (V x4 g))). app H24. app H12.
  cp (H14 _ H22). cp (worder_total H27). cp (total_order_pr1 H28 H23 H26). 
  nin H29.  red in H29. ee.  assert (inc x2 (substrate (V x0 g))). app H12.
  cp (H25 _ _ H31 H29).  assert (inc x3 x1). uf x1. inter2tac.
  cp (H20 _ H33). awi H34. rwi H2 H34. awi H34. am.  am. am. am.
  am. am. assert (gle (V x4 g) x2 x3). nin H29. red in H29.
  nin H29. red in H29. am. rw H29. nin H28;order_tac. 
  rwi H2 H30. awi H30. am. am. am. am. am. am. ufi x1 H19. inter2tac.
  eee. ir. nin (well_ordered_segment H7 H8). au. right.
  nin H9. nin H9. rwi H1 H9. nin (unionf_exists H9).  nin H11. exists x1.
  split. am. rw H10. wr (H5 _ _ H11 H12). app segment_is_segment. 
  red in H. ee. cp (H13 _ H11). nin H16;am.
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.*)

Lemma transfinite_principle1: forall  r s,
  worder r ->  (forall x, inc x s -> is_segment r x) ->
  (forall s', sub s' s -> inc (union s') s) ->
  (forall x, inc x (substrate r) -> inc (segment r x) s 
    -> inc (segment_c r x) s) ->
  (forall x, is_segment r x -> inc x s).
Proof. ir. assert (Ha: order r). nin H; am.
  cp (set_of_segments_worder H). 
  set (cs:= complement  (set_of_segments r) s). nin (emptyset_dichot cs).
  rwii inc_set_of_segments H3. assert (~ inc x cs). rw H5. red. ir. 
  elim (emptyset_pr H6). app (use_complement H3 H6). 
  red in H4. ee. awi H6.
  assert (sub cs (set_of_segments r)). uf cs. app sub_complement.
  nin (H6 _  H7 H5). red in H8. awi H8. ee.
  assert (sub x0 (substrate r)).  app sub_set_of_segments. app H7.
  assert (worder (induced_order r x0)). app worder_restriction. 
  nin (p_or_not_p (exists a, greatest_element (induced_order r x0) a)).
  ir. nin H12. red in H12. nin H12. awi H12. awi H13. 
  assert (x0 = segment_c r x1). 
  set_extens. cp (H13 _ H14). awi H15. rw segmentc_rw. am. app H10. am. am.  
  rwi segmentc_rw H14. cp (H7 _ H8). wri inc_set_of_segments H15. red in H15. 
  ee. app (H16 _ _ H12 H14). am.  app H10. 
  assert (inc x0 s). rw H14. app H2. app H10. 
  nin (p_or_not_p (inc (segment r x1) cs)). ir. cp (H9 _ H15). awi H16. ee.
  elim (not_in_segment (H18 _ H12)). am. am.
  ir. assert (inc (segment r x1)  (set_of_segments r)). wr inc_set_of_segments.
  app segment_is_segment. red in H12. ee. awi H12. app H10. am. 
  ufi cs H15. app (use_complement H16 H15). ufi cs H8. srwi H8.
  nin H8. elim H16. am.  am. am. am. am.
  ir. cp (worder_total H11). cp (union_segments H13). nin H14.
  assert (forall x : Set, ~ greatest_element (induced_order r x0) x). ir.
  red. ir. elim H12. exists x1. am. cp (H14 H16). clear H14; clear H15. awi H17.
  set (x1:= fun_image x0 (fun x => segment (induced_order r x0) x)).
  assert (forall z, inc z x1 -> inc z s). ir. unfold x1 in H14. awi H14.
  nin H14. nin H14.
  nin (inc_or_not z cs). ir. cp (H9 _ H18). awi H19. ee.
  cp (H21 _ H14). wri H15 H22. elim (not_in_segment H22). am. am. ir. 
  ufi cs H18. assert (inc z (set_of_segments r)).  wr inc_set_of_segments.
  assert (is_segment r x0). assert (inc x0 (set_of_segments r)). app H7.
  rw inc_set_of_segments. am. am. assert (is_segment (induced_order r x0) z).  
  wr H15. app segment_is_segment.  fprops. aw. 
  app (subsegment_is_segment Ha H19 H20). am. app (use_complement H19 H18).
  assert (inc (union x1) s). app H1. ufi x1 H15. rwi H17 H15.
  ufi cs H8. srwi H8.  nin H8. elim H18. am. am. am. fprops. aw.
Qed.

Lemma transfinite_principle2: forall  r s,
  worder r ->  (forall x, inc x s -> is_segment r x) ->
  (forall s', sub s' s -> inc (union s') s) ->
  (forall x, inc x (substrate r) -> inc (segment r x) s 
    -> inc (segment_c r x) s) ->
  inc (substrate r) s.
Proof. ir. cp  (transfinite_principle1 H H0 H1 H2).
  red in H. ee. cp (substrate_is_segment H). app H3.
Qed.

(** Two proofs of the transfinite principle; either by application of the
 previous lemma or direct proof *)
Theorem transfinite_principle: forall r (p:EP), 
  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. ir. set (s:= Zo (set_of_segments r)(fun z => forall y, inc y z -> p y)).
  assert (forall x, inc x s -> is_segment r x). uf s. ir. Ztac.
  wri inc_set_of_segments H3. am. am.
  assert (forall s', sub s' s -> inc (union s') s). uf s. ir. Ztac.
  wr inc_set_of_segments. app union_is_segment. red in H. eee.
  ir. cp (H3 _ H4). Ztac. clear H5. wri inc_set_of_segments H6. am. am. am. ir.
  nin (union_exists H4). nin H5. cp (H3 _ H6). Ztac. app H9.
  assert (forall x, inc x (substrate r) -> inc (segment r x) s -> 
      inc (segment_c r x) s).
  ir. ufi s H5. Ztac.  clear H5. assert (p x0). app H0.
  ir. app H7. rww segment_rw. uf s. Ztac. wr inc_set_of_segments. 
  app tack_on_segment. nin H; am. am. ir. 
  wri segment_c_pr H8. rwi tack_on_inc H8. nin H8. 
  app H7. rww H8. red in H; eee.  am. 
  cp (transfinite_principle2 H H2 H3 H4). ufi s H5. Ztac.  app H7.
Qed.

Theorem transfinite_principle_bis: forall r (p:EP), 
  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. ir. nin (p_or_not_p (p x)). tv. ir.
  set (X:=Zo (substrate r) (fun x => ~ p x)). assert (nonempty X). exists x.
  uf X. Ztac. assert (sub X (substrate r)).  uf X. app Z_sub.  red in H. ee. 
  nin (H5 _ H4 H3). red in H6. awi H6. ee. ufi X H6. Ztac. elim H9.
  app H0. ir. nin (p_or_not_p (p y)). tv. ir. assert (inc y X). uf X.
  clear H6. Ztac. cp ( H7 _ H13). awi H14.
  nin H11. elim H15. order_tac. am. am. am. am.
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). 
Definition restriction_to_segment_axiom r x g :=
  worder r & inc x (substrate r) & is_function g & sub (segment r x) (source g).

Lemma rts_function: forall r x g,  restriction_to_segment_axiom r x g  -> 
  is_function (restriction_to_segment r x g).
Proof. ir. red in H. ee. uf restriction_to_segment. app restriction1_function. 
Qed.

Lemma rts_W: forall r x g a,  restriction_to_segment_axiom r x g  -> 
  glt r a x -> W a  (restriction_to_segment r x g) = W a g.
Proof. ir. uf restriction_to_segment. red in H; ee.  app restriction1_W.
  uf segment. uf interval_uo. Ztac. order_tac. 
Qed.

Lemma rts_surjective: forall r x g,  restriction_to_segment_axiom r x g  -> 
  surjective(restriction_to_segment r x g).
Proof. ir. red in H. ee.  uf restriction_to_segment. 
  app restriction1_surjective. 
Qed.

Lemma rts_extensionality: forall r s x f g,
  worder r -> inc x (substrate r) -> worder s -> inc x (substrate s) ->
  segment r x = segment s x ->
  is_function f -> sub (segment r x) (source f) ->
  is_function g -> sub (segment s x) (source g) ->
  (forall a , inc a (segment r x) -> W a f = W a g) ->
  restriction_to_segment r x f = restriction_to_segment s x g.
Proof. ir. assert (restriction_to_segment_axiom r x f). red. eee.
  assert (restriction_to_segment_axiom s x g). red. eee.
  app function_exten. app rts_function. app rts_function.
  uf restriction_to_segment. uf restriction1. aw.
  uf restriction_to_segment. uf restriction1. aw.
  set_extens; awi H11; try am; nin H11; nin H11; aw; exists x1; wr H12;
  rw H8; try split; tv; ue. 
  ir. ufi restriction_to_segment H11. ufi restriction1 H11. awi H11.
  rw rts_W. rw rts_W. app H8. am. 
  rwi H3 H11. app (inc_segment H11). am. app (inc_segment H11). 
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.  *)

Definition transfinite_def r p f :=
  surjective f & source f = substrate r &
  forall x, inc x (substrate r) -> W x f = p (restriction_to_segment r x f).
Definition transfinite_defined r p:= choose (fun f => transfinite_def r p f).


Lemma transfinite_unique1: forall r p  f f' z, worder r ->
  inc z (substrate r) ->
  transfinite_def r p f -> transfinite_def r p f' -> 
  (forall x : Set, inc x (segment r z) -> W x f = W x f') ->
  restriction_to_segment r z f = restriction_to_segment r z f'.
Proof. ir. red in H1. red in H2. ee.
  assert (sub (segment r z) (substrate r)). app sub_segment.
  red in H1; red in H2; ee. app rts_extensionality. rww H6. rww H4.
Qed.

Lemma transfinite_unique: forall r p  f f', worder r -> 
  transfinite_def r p f -> transfinite_def r p f' -> f = f'.
Proof. ir. set (s:=Zo(set_of_segments r) (fun z =>
  forall x, inc x z -> W x f = W x f')).
  assert (Ha: worder r). am. red in H. ee. clear H2.
  assert (Hb: forall x, inc x s -> is_segment r x). uf s. ir. Ztac. 
  rww inc_set_of_segments.
  assert (Hc:forall s', sub s' s -> inc (union s') s). ir. uf s. Ztac. 
  wr inc_set_of_segments. app union_is_segment. ir. app Hb. app H2. am. 
  ir.  nin (union_exists H3). ee. cp (H2 _ H5). ufi s H6. Ztac. app H8.
  assert (Hd: forall x, inc x (substrate r) -> inc (segment r x) s 
    -> inc (segment_c r x) s). ir. uf s. Ztac. 
  wr inc_set_of_segments. app tack_on_segment. am. ir. ufi s H3. Ztac.
  wri segment_c_pr H4. rwi tack_on_inc H4. nin H4. app H6. rw H4. 
  cp (transfinite_unique1 Ha H2  H0 H1 H6).
  red in H0. ee. rw H9. red in H1. ee. rw H11. rww H7. am. am. am. am.
  cp (transfinite_principle2 Ha Hb Hc Hd). ufi s H2. Ztac. 
  red in H0; red in H1; ee. app function_exten.
  red in H0; eee. red in H1; eee. rww H5.  set_extens.
  cp (surjective_pr2 H0 H9). nin H10.  nin H10. rwi H7 H10. 
  wr H11. rw H4. app inc_W_target. red in H1; ee;am. rww H5. am. 
  cp (surjective_pr2 H1 H9). nin H10.  nin H10. rwi H5 H10. 
  wr H11. wr H4. app inc_W_target. red in H0; eee.  ue. am. ue.
Qed.

Lemma transfinite_pr: forall r x p, worder r -> transfinite_def r p x ->
  transfinite_defined r p = x.
Proof. ir.  assert (transfinite_def r p  (transfinite_defined r p)).
  uf transfinite_defined.  app choose_pr.  exists x. am.
  app (transfinite_unique H H1 H0).
Qed.

Lemma transfinite_aux1: forall r p s' s'' f' f'',
  worder r -> is_segment r s' -> is_segment 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. ir. set (f:=restriction1 f'' s').
  assert (Ha:order r). red in H; eee.
  assert (Hb: sub s'' (substrate r)).  red in H1. eee.
  assert (Hc:is_function f''). red in H4;ee. red in H4;eee.
  assert (Hd: sub s' (substrate r)). red in H0. eee.
  assert (He: worder (induced_order r s')). app worder_restriction.
  assert (Hf: sub s' (source f'')). nin H4. ee. awi H5. rww H5. nin H; am. am.
  assert (Hg: source f = s'). uf f. uf restriction1. aw.
  assert (transfinite_def (induced_order r s') p f). 
  assert (is_function f). uf f.  app restriction1_function. 
  assert (surjective f). uf f. app restriction1_surjective.
  red. split. am. split. rw Hg. aw. ir. awi H7. 
  assert (sub (segment (induced_order r s') x) s'). app sub_segment2.
  assert (sub (segment (induced_order r s'') x) (source f'')). 
  red in H4. ee. rw H9. app sub_segment. 
  assert (forall a, inc a s' -> W a f = W a f''). uf f. ir. rww restriction1_W. 
  assert (restriction_to_segment (induced_order r s') x f =
    restriction_to_segment (induced_order r s'') x f'').
  app rts_extensionality. aw. app worder_restriction. 
  aw. app H2. rww segment_induced_a. rww segment_induced_a. app H2. rww Hg. 
  ir.  app H10.  app H8. rw H11. rw H10. red in H4. ee. app H13. aw. 
  app H2. am. am. am. app (transfinite_unique He H3 H5).
Qed. 
  

Lemma transfinite_aux2: forall r p s tdf, worder r ->
  (forall z, inc z s -> is_segment r z) ->
  (forall z, inc z s ->  transfinite_def (induced_order r z) p (tdf z)) ->
  exists f, 
    (transfinite_def (induced_order r (union s)) p f &
      target f = unionf s (fun z => target (tdf z))).
Proof. ir. assert (Hx: order r). red in H; eee.
  assert (Hb:forall i, inc i s -> is_function (tdf i)). ir. nin (H1 _ H2).
  ee. fct_tac.
  assert (He:forall i, inc i s -> source (tdf i) = i). ir. cp (H1 _ H2).
  red in H3. ee. rw H4. cp (H0 _ H2). red in H6. ee. aw. 
  set (t:=unionf s (fun z => target (tdf z))).
  set (tde:= fun z => corresp (source (tdf z)) t (graph (tdf z))).
  assert (Ha:forall i, inc i s -> function_prop (tde i) i t). ir.
  cp (Hb _ H2). uf tde. red. aw. ee. red in H3. ee. app is_function_pr. 
  apply sub_trans with (target (tdf i)). fprops. uf t. red. ir. union_tac.
  app He. tv.
  assert (forall i a, inc i s-> inc a i -> W a (tdf i) = W a (tde i)).
  ir. set (x:= W a (tde i)). assert (inc (J a x) (graph (tde i))). uf x.
  nin (Ha _ H2). app W_pr3. eee. ufi tde H4. awi H4. app W_pr.  app Hb.
  assert (forall i j, inc i s -> inc j s -> sub i j ->
    agrees_on (intersection2 i j) (tde i) (tde j)).
  ir. assert (intersection2 i j = i).  set_extens. inter2tac. 
  app intersection2_inc. app H5.  rw H6. red.
  cp (Ha _ H3). cp (Ha _ H4). red in H7; red in H8. eee.  ir. wrr H2. wrr H2.
  cp (transfinite_aux1 H (H0 _ H3)  (H0 _ H4)  H5 (H1 _ H3) (H1 _ H4)).
  rw H14. rww restriction1_W. app Hb. rw He. am. am. app H5. 
  assert (Hd:forall i j, inc i s -> inc j s -> 
    agrees_on (intersection2 i j) (tde i) (tde j)). ir.
  nin (segment_dichot_sub H (H0 _ H4) (H0 _ H5)). app H3. rw intersection2comm.
  cp (H3 _ _ H5 H4 H6). red in H7. red. eee. ir. sy. app H9.
  assert (Hc:sub (union s) (substrate r)). red. ir. nin (union_exists H4).
  ee. cp (H0 _ H6). red in H7. nin H7. app H7.
  nin (extension_covering _ _ Ha Hd). clear H5. nin H4.
  assert (Hf:forall x0 x1, inc x0 x1 -> inc x1 s -> sub
    (segment (induced_order r (union s)) x0) x1).
  ir. red. ir. cp (H0 _ H6). red in H8. ee. cp (inc_segment H7).
  nin H11. cp (related_induced_order1 H11). app (H9 _ _ H5 H13).
  nin H4. ee. red in H4. ee. exists x. split. red. split. app surjective_pr6.  
  ee. ir. rwi H7 H8. ufi t H8. nin  (unionf_exists H8). nin H9.
  nin (H1 _ H9). cp (surjective_pr2 H11 H10). nin H13. nin H13. rwi He H13. 
  assert (inc x1 (source x)). rw H6. union_tac. ex_tac.
  cp (H5 _ H9). red in H16. ee. rw H18. wr H2. am. am. am. am. am.
  split. aw. wri union_prop H6. am.  
  ir. awi H8. nin (union_exists H8). nin H9.
  assert (Hg:forall a, inc a x1 -> W a x = W a (tdf x1)). ir.
  cp (H5 _ H10). red in H12. ee. rw H14. sy. app H2. am. rw Hg.
  assert (restriction_to_segment (induced_order r (union s)) x0 x =
    restriction_to_segment (induced_order r x1) x0 (tdf x1)).
  assert (sub x1 (substrate r)). cp (H0 _ H10). red in H11. ee. am.
  app rts_extensionality. app worder_restriction.  aw. app worder_restriction.
  aw. assert (segment (induced_order r x1) x0 = segment r x0).
  rww segment_induced_a. app H0. rw H12. clear H12.
  set_extens. rw segment_rw. cp (inc_segment H12). 
  cp (related_induced_order2  H13). am. app H11.
  rw segment_rw. cp (inc_segment H12). red in H13. red. ee.
  rw related_induced_order. am. apply union_inc with x1.
  cp (H0 _ H10). red in H15. ee. app (H16 _ _ H9 H13). am. am. am. aw.
  rw H6. red. ir. union_tac. app (Hf _ _ H9 H10).
  app Hb. rw He. app sub_segment2. am. ir. app Hg. app (Hf _ _ H9 H10).
  rw H11. cp (H1 _ H10). red in H12. ee. app H14. aw. cp (H0 _ H10).
  red in H15. ee. am. am. am. am. am.  
Qed. 


Lemma transfinite_aux3: forall 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 (segment_c r x)) p 
    (tack_on_f g x (p (restriction_to_segment r x g))).
Proof. ir. cp H1. assert (order r). red in H; eee.
  assert (sub (segment r x) (substrate r)). app sub_segment.
  assert(substrate (induced_order r (segment r x)) = segment r x). aw.
  red in H1. ee. rwi H5 H6. rwi H5 H7.
  set (tsx:= segment_c r x). assert (sub tsx (substrate r)). uf tsx. 
  app sub_segmentc. 
  assert(substrate (induced_order r tsx) = tsx). aw.
  assert (~ (inc x (source g))). rw H6. aw. red. ir. app (not_in_segment H10). 
  cp (tack_on_surjective  (p (restriction_to_segment r x g)) H1 H10).
  red in H1. ee. clear H12. assert (Hu:tack_on (segment r x) x = tsx).
  uf tsx. rww segment_c_pr. red. eee.
  uf tack_on_f. simpl. rw H6. aw. red in H11. ee. clear H12. ir. awi H12.
  assert (sub (segment r x0) (segment r x)). app segment_monotone.
  ufi tsx H12. wrr segmentc_rw. assert (Hx: inc x0 tsx). am. ufi tsx H12. 
  rwi segmentc_rw H12.  nin (equal_or_not x0 x). rw H14. 
  rw tack_on_W_out. assert (sub (segment r x) tsx). wr Hu. fprops. rwi H14 Hx.
  assert  (segment (induced_order r tsx) x = segment r x).
  app segment_induced_a. uf tsx. app tack_on_segment.
  assert (restriction_to_segment r x g = restriction_to_segment 
    (induced_order r tsx) x (tack_on_f g x (p (restriction_to_segment r x g)))).
  app rts_extensionality. app worder_restriction. rww H9. sy. am. rw H6. 
  fprops. uf tack_on_f. aw. rw H16. rw H6. fprops.
  ir. rw tack_on_W_in. tv. am. am. rww H6. wrr H17. am. am. 
  assert (glt r x0 x). red. eee.
  cp (segment_induced H3 H15). cp (segment_induced1 H3 H15). 
  assert (inc x0 (segment r x)). app segment_inc. cp (H7 _ H18).
  set (k:= (tack_on_f g x (p (restriction_to_segment r x g)))).
  assert (source k = tsx). uf k. uf tack_on_f. aw. rw H6. am.
  assert (forall u, inc u (segment r x) -> W u g = W u k). ir.
  uf k. rw tack_on_W_in. tv. am. am. rww H6. wr H21.
  assert (restriction_to_segment (induced_order r  (segment r x)) x0 g = 
    restriction_to_segment (induced_order r tsx) x0 k).
  app rts_extensionality.  app worder_restriction. rww H5. 
  app worder_restriction. rww H9.  rw H16. uf tsx.  rww H17. rw H16. rw H6. am. 
  uf tsx. rww H17. rww H20. apply sub_trans with (segment r x).
  am. wr Hu.  fprops. ir. app H21.  cp (sub_segment H22). awi H23. am. am.
  am. wr H22. am. am. am. am. am.
Qed.


Theorem transfinite_definition: forall r p,
  worder r -> exists_unique (fun f => transfinite_def r p f).
Proof. ir. set (s:=Zo(set_of_segments r) (fun z => 
  exists f, transfinite_def (induced_order r z)  p f)).
  assert (Ha : order r). nin H; am.
  assert (Hb: forall x, inc x s -> is_segment r x).  uf s. ir. Ztac. 
  wrii inc_set_of_segments H1. 
  assert (inc (substrate r) s). app transfinite_principle2. ir. uf s. Ztac. 
  wr inc_set_of_segments. app union_is_segment. ir. app Hb. app H0. am.
  set(tdf:= fun z => transfinite_defined (induced_order r z) p).
  assert (forall x : Set, inc x s' -> is_segment r x). ir. app Hb. app H0.
  assert (forall z, inc z s' -> transfinite_def (induced_order r z) p (tdf z)).
  ir. cp (H0 _ H2). ufi s H3. Ztac.  uf tdf. app (choose_pr H5).
  cp (transfinite_aux2 _ H H1 H2). nin H3. ee. exists x. am. ir. 
  ufi s H1. Ztac. nin H3. uf s. clear H1. Ztac. wr inc_set_of_segments. 
  app tack_on_segment. am. set (transfinite_aux3 H H0 H3).
  exists (tack_on_f x0 x (p (restriction_to_segment r x x0))). am.
  ufi s H0. Ztac. nin H2. rwi induced_order_substrate H2.
  red. ee. exists x. am. ir. app (transfinite_unique H H3 H4). am.
Qed.

Theorem transfinite_definition_stable: forall r p F,
  worder r ->
  (forall f, is_function f -> is_segment r (source f) -> sub (target f) F ->
    inc (p f) F) ->
  sub (target (transfinite_defined r p)) F.
Proof. ir. set (s:=Zo(set_of_segments r) (fun z => 
  exists f, (transfinite_def (induced_order r z)  p f) & (sub (target f) F))).
  assert (Hx:order r). nin H; am.
  assert (Hb: forall x, inc x s -> is_segment r x).  uf s. ir. Ztac. 
  wrii inc_set_of_segments H2. 
  assert (inc (substrate r) s). app transfinite_principle2. ir. uf s. Ztac. 
  wr inc_set_of_segments. app union_is_segment. ir. app Hb. app H1. am. 
  set(tdf:= fun z => transfinite_defined (induced_order r z) p).
  assert (forall x : Set, inc x s' -> is_segment r x). ir. app Hb. app H1.
  assert (forall z, inc z s' -> transfinite_def (induced_order r z) p (tdf z)).
  ir. cp (H1 _ H3). ufi s H3. Ztac.  uf tdf.  ufi s H4. Ztac.
  assert (exists f, transfinite_def (induced_order r z) p f). nin H6. ee.
  exists  x. am. app (choose_pr H7).
  cp (transfinite_aux2 _ H H2 H3). nin H4. ee.  exists x. eee. 
  red. ir.  nin (unionf_exists H6). ee.  cp (H1 _ H7). ufi s H9. Ztac.
  nin H11. nin H11. cp (H3 _ H7). 
  assert (worder (induced_order r x1)). app worder_restriction. cp (H2 _ H7).
  app sub_segment1.  cp (transfinite_unique H14 H11 H13).  rwi H15 H12. app H12.
  ir.  ufi s H2. Ztac. nin H4. ee. uf s. clear H2. Ztac.
  wr inc_set_of_segments. app tack_on_segment. am.
  set (transfinite_aux3 H H1 H4).
  exists  (tack_on_f x0 x (p (restriction_to_segment r x x0))). split. am.
  assert (sub (segment r x) (substrate r)).  app sub_segment. 
  red in H4. clear t. ee. uf tack_on_f. aw. red. ir.
  rwi tack_on_inc H8. nin H8. app H5. rw H8. app H0. 
  app rts_function. red. eee. fct_tac. aw. fprops.
  uf restriction_to_segment. uf restriction1. aw.
  app segment_is_segment.  uf restriction_to_segment. uf restriction1. aw.
  red. ir. app H5.
  ufi image_by_fun H9. awi H9. nin H9. nin H9.
  red in H4. ee.  app (inc_pr2graph_target  H4 H10). 
  ufi s H1. Ztac.  nin H3. ee. assert (induced_order r (substrate r) =r).
  app induced_order_substrate.   assert (transfinite_defined r p = x). 
  rwi H5 H3. app (transfinite_pr H H3). ue. 
Qed.

Lemma transfinite_defined_pr: forall r p, worder r ->
  transfinite_def r p  (transfinite_defined r p).
Proof. ir.  uf transfinite_defined. app choose_pr. 
  nin (transfinite_definition p H). am.
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 (intersection2 (substrate r) (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: forall r r',
  common_ordering_set r r' = common_ordering_set r' r.
Proof. ir. uf common_ordering_set. rw intersection2comm.
  set_extens; Ztac; eee. 
Qed.

Lemma Zermelo_aux1: forall r r', worder r ->  worder r' ->
  is_segment r (common_ordering_set r r').
Proof. ir. uf common_ordering_set. red. split. red. ir. Ztac. inter2tac.
  ir. nin (equal_or_not y x). rww H3. cp (Z_all H1). ee. clear H1.
  nin (intersection2_both H4).
  assert (inc y (segment r x)). rw segment_rw. split; am. am.
  cp (inc_arg1_substrate H2). 
  assert (inc y (substrate r')). rwi H5 H8. app (sub_segment H8).  
  ufi induced_order H6. wri H5 H6. set (cs:= coarse (segment r x)) in *.
  assert (segment r y = segment r' y). nin H. nin H0.
  set_extens; app segment_inc; cp (inc_segment H13); nin H14;
    [set (le_in_segment H H1 H8 H14) |
      rwi H5 H8; set (le_in_segment H0 H7 H8 H14)];
    split; tv; red; red;  cut (inc (J x0 y) (intersection2 r cs)). 
  ir.   rwi H6 H16. inter2tac. inter2tac. uf cs.  uf coarse. fprops.
  ir. inter2tac. rw H6. inter2tac. uf cs.  rw H5. uf coarse. fprops.
  Ztac. inter2tac. eee. wr H11. uf induced_order. 
  nin H. cp (coarse_segment_monotone H H2). fold cs in H13.
  set_extens; nin (intersection2_both H14);
  assert (inc x0 (intersection2 r cs)). fprops. inter2tac.
  app H13. rwi H6 H17. inter2tac. inter2tac.
  assert (inc x0 (intersection2 r' cs)).
  inter2tac. app H13. wri H6 H17.  am.  inter2tac. inter2tac.
Qed.

Lemma Zermelo_aux2: forall r r' v, worder r ->  worder r' ->
  v = common_ordering_set r r' ->  sub(induced_order r v) (induced_order r' v).
Proof. ir. uf induced_order. ufi common_ordering_set H1. uf coarse. red. ir.
  nin (intersection2_both H2).  inter2tac. awi H4. ee. 
  assert (J (P x) (Q x) = x). aw. rwi H1 H6. Ztac. ee.
  nin (intersection2_both H8). 
  nin (equal_or_not (P x) (Q x)). wr H7. rw H13. nin H0. order_tac.
  assert (inc (P x) (segment r (Q x))). app segment_inc. split.
  red. red. rww H7. am.
  rwi H9 H14.  cp (inc_segment H14). nin H15. eee. 
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: forall E s p r r', 
  let q := fun r r' => sub (substrate r) (substrate r') 
    & r = induced_order r' (substrate r) & is_segment r' (substrate r) in
    Zermelo_axioms E p s r -> Zermelo_axioms E p s r' ->
    q r r' \/ q r' r.
Proof. ir. assert (Ha:worder r). ufi Zermelo_axioms H. eee. 
  assert (Hb:worder r'). ufi Zermelo_axioms H0. eee.
  cp (Zermelo_aux1 Ha Hb). cp (Zermelo_aux1 Hb Ha). rwi Zermelo_aux0 H2.
  set (v:=  common_ordering_set r r') in *. 
  assert (induced_order r v = induced_order r' v). ap extensionality;
  app Zermelo_aux2. rww Zermelo_aux0. 
  cp (sub_segment1 H1). cp (sub_segment1 H2).
  nin (equal_or_not v (substrate r)). left. uf q. wr H6. eee.
  wr H3. rw H6. sy. app induced_order_substrate. nin Ha; am.  
  nin (equal_or_not v (substrate r')). right. uf q. wr H7. eee. 
  rw H7. sy. app induced_order_substrate. nin Hb; am. 
  nin (emptyset_dichot  (complement (substrate r) v)). elim H6.
  app extensionality. app empty_complement. 
  nin (emptyset_dichot (complement (substrate r') v)). elim H7.
  app extensionality. app empty_complement. 
  assert (sub  (complement (substrate r) v) (substrate r)). app sub_complement.
  assert (sub (complement (substrate r') v) (substrate r')). app sub_complement.
  cp (worder_total Ha). cp (worder_total Hb). red in Ha; red in Hb; ee.
  nin (H17 _  H10 H8). nin (H15 _  H11 H9).
  assert (Hw:inc x (substrate r)). nin H18. awi H18. srwi H18. ee. am. am. am.
  assert (Hv:inc x0 (substrate r')). nin H19. awi H19. srwi H19. ee. am. am. am.
  assert (segment r x = v).  
  set_extens. ex_middle. ir. cp (inc_segment H20). 
  assert (inc x1 (complement (substrate r) v)). srw. split. order_tac. am.
  red in H18. ee. awi H24. cp (H24 _ H23). 
  cp (related_induced_order1 H25). order_tac. am. am. 
  rw segment_rw. assert (inc x1 (substrate r)). app H4.
  nin (total_order_pr2 H12 H21 Hw). am. red in H1. ee. cp (H23 _ _ H20 H22). 
  red in H18. ee. awi H19. awi H18. srwi H18. ee. elim H26. am. 
  am. am. am.
  assert (segment r' x0 = v).  
  set_extens. ex_middle. ir. cp (inc_segment H21). 
  assert (inc x1 (complement (substrate r') v)). srw. split. order_tac. am.
  red in H19. ee. awi H25. cp (H25 _ H24). 
  cp (related_induced_order1 H26). order_tac. am. am. 
  rw segment_rw. assert (inc x1 (substrate r')). app H5.
  nin (total_order_pr2 H13 H22 Hv). am. red in H2. ee. cp (H24 _ _ H21 H23). 
  red in H19. ee. awi H19. srwi H19. ee. elim H27. am. am. am. am.
  red in H. red in H0. ee. cp (H27 _ Hw). cp (H24 _ Hv). 
  rwi H20 H28. rwi H21 H29. rwi H28 H29.
  assert (inc x v). uf v. uf common_ordering_set. Ztac.
  inter2tac. rww H29. ee. rw H20. rw H29. rw H21. tv.
  rw H20. rw H29. rw H21. am. wri H20 H30. elim (not_in_segment H30).
Qed.


Lemma Zermelo_aux4: forall r a, worder r ->
  let owg := order_with_greatest r a in
    ~ (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. ir. cp (worder_adjoin_greatest H H0). 
  nin H. cp (order_with_greatest_pr H H0).  uf owg. ee. am.
  set_extens. cp (inc_segment H7). cp (inc_lt1_substrate H8). rwi H4 H9. 
  rwi tack_on_inc  H9. nin H9. am. nin H8. contradiction.
  red in H6. ee. rwi H4 H8.  rw segment_rw. red. ee. app H8. fprops. red. ir. 
  rwi H9 H7. contradiction. am. ir. rwi H4 H7. rwi tack_on_inc H7. 
  nin H7. right. set_extens. cp (inc_segment H8). red in H9. nin H9.
  red in H9. red in H9. ufi order_with_greatest H9.
  nin (union2_or H9). rw segment_rw. red. au. am. 
  awi H11. ee. awi H13. rwi H13 H7. contradiction.
  cp (inc_segment H8). rw segment_rw. red in H9. red. ee. red. red. 
  uf order_with_greatest. app union2_first. am. ue. au. 
Qed.

Lemma Zermelo_aux:  forall E s p, sub s (powerset E) ->
  (forall x, inc x s -> (inc (p x) E & ~ (inc (p x) x))) ->
  exists r, Zermelo_axioms E p s r & (~  (inc (substrate r)  s)).
Proof. ir. 
  set (m:= Zo (powerset (coarse E)) (fun r => Zermelo_axioms E p s r)).
  set (q := fun r r' => sub (substrate r) (substrate r') 
    & r = induced_order r' (substrate r) & is_segment r' (substrate r)).
  assert(forall r r', inc r m -> inc r' m -> q r r' \/ q r' r). uf q. ir.
  ufi m H1. ufi m H2. order_tac. app (Zermelo_aux3 H4 H6). 
  set (g:= L m (fun z => z)).  assert (common_worder_axiom g). uf g. red. ee.
  gprops. ir. bwi H2. bw. ufi m H2. Ztac.
  red in H4. ee. am. bw. ir. bw.  ufi m H2. ufi m H3. order_tac.
  cp (Zermelo_aux3 H5 H7).  nin H2;ee; au. 
  bw. ir. bw. bwi H4. ufi m H2. ufi m H3. order_tac.
  cp (Zermelo_aux3 H6 H8). nin  H2. ee. am. ee.
  assert (substrate a = substrate b). app extensionality. rw H10.
  rw induced_order_substrate. rw H3. wr H10. rww induced_order_substrate. 
  destruct H6 as [[G  _] _]. am. destruct H8 as [[G  _] _]. am.
  am. am.  cp (worder_merge H2). ee. red in H3. ee.
  assert (domain g = m). uf g. bw.
  assert (forall a, inc a m -> V a g = a). ir. uf g. bw. rewrite H10 in *.
  set (m0:= unionb g). fold m0 in  H3, H4, H5, H6, H7, H8, H9.
  assert (Zermelo_axioms E p s m0). red. ee. am. rw H8.  
  red. ir. nin (unionf_exists H12). ee. rwi H11 H14. ufi m H13. Ztac. 
  red in H16. ee.  app H17. am. ir.  rwi H8 H12. nin (unionf_exists H12). ee.
  wr (H6 _ _ H13 H14).  rwi H11 H14. rw H11. ufi m H13. Ztac. red in H16.
  eee. am. am. ir. rwi H8 H12. nin (unionf_exists H12). ee.
  wr (H6 _ _ H13 H14).  rwi H11 H14. rw H11. ufi m H13. Ztac. red in H16. eee.
  am. am. exists m0. eee.
  nin (inc_or_not (substrate m0) s). ir.
  set (a:= p (substrate m0)). cp (H0 _ H13). fold a in H14. nin H14.
  cp (Zermelo_aux4 H4 H15). ee. cp (order_with_greatest_pr H3 H15). 
  assert (Zermelo_axioms E p s (order_with_greatest m0 a)). red. ee.
  am. ee. rw H20. red. ir.
  rwi tack_on_inc H23. nin H23. red in H12. eee. ue. ir.
  nin (equal_or_not x a). rww H24. rww H17.
  nin (H18 _ H23). elim H24. am. rw H25. red in H12. ee. app H27. rwi H20 H23.
  rwi tack_on_inc  H23. nin H23. am. elim H24. am. 
  ir. nin (equal_or_not x a). rww H24. rww H17.
  nin (H18 _ H23). elim H24. am. rw H25. red in H12. ee. app H28. rwi H20 H23.
  rwi tack_on_inc  H23. nin H23. am. elim H24. am. 
  assert (inc (order_with_greatest m0 a) m). uf m. Ztac.
  app powerset_inc. 
  apply sub_trans with (coarse (substrate (order_with_greatest m0 a))).
  app sub_graph_coarse_substrate. nin H19; fprops.
  assert (sub (substrate (order_with_greatest m0 a)) E). red in H20; eee.
  uf coarse. app product_monotone. red in H2.
  assert (inc a (substrate m0)). rw H8. 
  apply unionf_inc with (order_with_greatest m0 a).  am.  rw H11. eee. 
  am. contradiction.  am. 
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: forall E, exists r, worder r & substrate r = E.
Proof. ir. set (s:=complement (powerset E) (singleton E)).
  assert (sub s (powerset E)). uf s. app sub_complement.
  set (p:= fun x => rep (complement E x)).
  assert (forall x, inc x s -> inc (p x)  (complement E x)). ir. uf p.
  app nonempty_rep. app strict_sub_nonempty_complement. ufi s H0. srwi H0.
  ee. split. red. ir. elim H1. rw H2. fprops. app powerset_sub.  
  assert (forall x, inc x s -> (inc (p x) E & ~ (inc (p x) x))). ir.  
  cp (H0 _ H1). srwi H2. am. 
  cp (Zermelo_aux p H H1).  nin H2. ee. exists x. red in H2. eee.
  assert (inc (substrate x) (complement (powerset E) s)). srw. 
  ee. app powerset_inc. am. ufi s H7.
  rwi double_complement H7.  app singleton_eq. red. ir. 
  rw (singleton_eq H8).  app inc_x_powerset_x.
Qed.


Lemma Zermelo_bis: forall E, exists r, worder r & substrate r = E.
Proof. ir. set (prec := fun a => complement a (singleton (rep a))).
  assert (Ha: prec emptyset = emptyset). app is_emptyset. ir. red. ir.
  ufi prec H. srwi H. nin H. elim (emptyset_pr H).
  assert (Hb: forall a, sub (prec a) a). ir. uf prec. app sub_complement.
  set (chain:= fun F => sub F (powerset E) & inc E F & 
    (forall A, inc A F -> inc (prec A) F) 
    & (forall A, sub A F -> nonempty A -> inc (intersection A) F)).
  assert (Hc:chain (powerset E)). red. ee. fprops. app powerset_inc. fprops.
  ir. app powerset_inc. apply sub_trans with A. app Hb. rwi powerset_inc_rw H.
  am. ir. app powerset_inc. red. ir. nin H0. cp (intersection_forall H1 H0).
  cp (H _ H0). rwi powerset_inc_rw H3. app H3.
  set (om:= intersection (Zo (powerset (powerset E)) chain)).
  assert (Hd:chain om).  assert (nonempty (Zo (powerset (powerset E)) chain)).
  exists (powerset E). Ztac. app powerset_inc. fprops. red. uf om. ee.
  app intersection_sub. Ztac.  app powerset_inc. fprops.  
  app intersection_inc. ir. Ztac. red in H2. ee. am. ir.
  app intersection_inc. ir. Ztac. red in H3. ee. app H5. 
  ap (intersection_forall H0 H1). ir. app intersection_inc. ir. Ztac.
  red in H4. ee. app H7. red. ir. cp (H0 _ H8).
  app (intersection_forall H9 H2).
  assert (He: forall x, chain x -> sub om x). ir. uf om. app intersection_sub.
  Ztac. red in H. ee. app powerset_inc.
  set (m:= fun a => forall x, inc x om -> sub x a \/ sub a x).
  assert (Hf: om = Zo om m). app extensionality. app He. red in Hd.  red. ee.
  apply sub_trans with om. app Z_sub. am. Ztac. uf m. ir. left. 
  cp (H _ H3). app powerset_sub. ir. Ztac. clear H3. red in H5. Ztac.
  assert (sub om (Zo om (fun x=> sub x (prec A) \/ sub A x))).
  app He. red. ee. apply sub_trans with om. app Z_sub. am. Ztac.  right.
  app powerset_sub. app H. ir. Ztac. clear H3. Ztac. nin H7. left.
  apply sub_trans with A0. app Hb. am. cp (H1 _ H6). nin (H5 _ H7).
  nin (inc_or_not (rep A0) A). assert (sub A0 A).  ufi prec H8. red. ir.
  nin (equal_or_not x (rep A0)). rw H11. am. app H8. srw. ee. am. red. ir.
  awi H12. contradiction. assert (A0 = A). app extensionality. rw H11. left.
  fprops. right. red. ir. uf prec. srw. ee. app H3. red. ir. awi H11. 
  rwi H11 H10. contradiction. au. ir. Ztac. app H2. eapply sub_trans. eexact H3.
  app Z_sub. nin (p_or_not_p (exists x, inc x A0 & sub x (prec A))).
  nin H7. left. red. ir. ee.  app H9. app (intersection_forall H8 H7).
  right. red. ir. app intersection_inc. ir. cp (H3 _  H9). Ztac. nin H12.
  elim H7. ex_tac. app H12. red. ir. nin (H5 _ H6). cp (H3 _ H6). Ztac. nin H10.
  au. right. assert (A = x). app extensionality. rw H11. app Hb. right.
  apply sub_trans with A. app Hb. am.
  ir. Ztac. app H2. eapply sub_trans. eexact H3. app Z_sub. red. ir.
  nin (p_or_not_p (exists y, inc y A & sub y x)).
  nin H6. right. red. ir. ee. app H8. app (intersection_forall H7 H6).
  left. red. ir. app intersection_inc. ir. cp (H3 _  H8). Ztac.  
  nin (H11 _ H5). app H12. elim H6. ex_tac.  app Z_sub.
  assert (Hg: forall a b, inc a om -> inc b om -> sub a b \/ sub b a).
  ir. rwi Hf H0. Ztac. ap (H2 _ H).
  set (d:= fun p => intersection (Zo om (fun x => sub p x))).
  assert (Hh: forall p, sub p E -> inc (d p) om). ir. red in Hd. ee. 
  uf d. app  H3. app Z_sub. exists E. Ztac.
  assert (Hi: forall p, sub p E -> sub p (d p)). ir. uf d. red. ir.
  app intersection_inc. exists E. Ztac.  red in Hd; ee;am. ir. Ztac. app H3.
  assert (Hj: forall p q, inc q om -> sub p q -> sub p E-> sub (d p) q).
  ir. uf d. app intersection_sub. Ztac.
  assert (Hk: forall p, sub p E -> nonempty p -> inc (rep (d p)) p). ir.
  nin (inc_or_not (rep (d p)) p). am. assert (sub p (prec (d p))).
  red. ir. uf prec. srw. split. app (Hi _ H). red. ir. awi H3. rwi H3 H2.
  contradiction. red in Hd. ee. cp (H5 _ (Hh _ H)). cp (Hj _ _ H7 H2 H).
  ufi prec H8.  nin (emptyset_dichot (d p)).
  rwi H9 H2. rwi Ha H2. nin H0. elim (emptyset_pr (x:= y)). app H2.
  cp (nonempty_rep H9). cp (H8 _ H10). srwi H11. ee. awi H12. elim H12. tv.
  assert (Hl: forall p q, inc q om -> sub p q -> inc (rep q) p -> q = d p).
  ir. nin Hd. ee.  assert (sub p E). apply sub_trans with q. am.  
  app powerset_sub. app H2.  cp (Hj _ _ H H0 H6). 
  nin (Hg _ _  (Hh _ H6) (H4 _ H)). cp (Hi _ H6). assert (inc (rep q) (prec q)).
  app H8. app H9. ufi prec H10. srwi H10. nin H10. awi H11. elim H11. tv.
  app extensionality. red. ir. nin (equal_or_not x (rep q)).
  app (Hi _ H6). ue. app H8. uf prec. srw. ee. am. aw.
  set (R:= fun x => d (singleton x)).
  assert (Hm:forall x, inc x E -> 
    (inc (R x) om & inc x (R x) &  rep (R x) = x)). ir. uf R.
  assert (sub (singleton x) E). app sub_singleton. cp (Hi _ H0). ee. app Hh.
  app H1. fprops. assert (nonempty (singleton x)). exists x.  fprops.
  cp (Hk _ H0 H2). awi H3. am.
  assert (Hn:forall x y, inc x E -> inc y E -> R x = R y -> x = y). ir.
  cp (Hm _ H). cp (Hm _ H0). ee. wr H7; wr H5. rww H1.
  assert (Ho: forall q, inc q om -> nonempty q -> R (rep q) = q). ir.
  uf R. sy. app Hl. red. ir. awi H1. rw H1. app nonempty_rep. fprops.
  assert (Hp: forall x y, inc x E -> inc y E -> inc x (R y) ->
    (sub (R x) (R y))). ir.  cp (Hm _ H0); ee.   cp (Hm _ H); ee. 
  nin (Hg _ _ H5 H2). am.
  assert (sub (doubleton x y) (R y)). red. ir. nin (doubleton_or H9). ue. ue.
  assert (sub (doubleton x y) (R x)). apply sub_trans with (R y). am. am.
  assert (inc (rep (R x)) (doubleton x y)).  rw H7. fprops.
  assert (inc (rep (R y)) (doubleton x y)).  rw H4. fprops.
  cp (Hl _ _ H5 H10 H11). cp (Hl _ _ H2 H9 H12). rw H13; rw H14. fprops.
  set (r := graph_on (fun x y => (sub (R y) (R x))) E).
  assert (Hq:order r). uf r. app order_from_rel1. red. ir. eee.
  apply sub_trans with (R y). am. am. ir. eee. ir. app Hn. 
  app extensionality. ir. fprops.
  assert (Hs:substrate r = E). uf r. rww substrate_graph_on. ir. fprops.
  exists r. split. split. am. rw Hs. ir. cp (Hk _ H H0).
  exists (rep (d x)). red. aw. ee. am. ir. aw. uf r. 
  rww graph_on_rw1. ee. app H. app H. app Hp. app H. app H.
  cp (Hi _ H). rw Ho.  app H3. app Hh. nin H0. exists y.
  app H3. rww Hs. am.
Qed.


(** **  EIII-2-4 Inductive sets *)

Definition inductive_set 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: forall a b,
  inductive_set (opposite_order (extension_order a b)).
Proof. ir. cp (extension_is_order a b). red. ir. red in H1. ee. awii H2. 
  awi H0. 
  assert (Ha:forall i, inc i X -> is_function i). ir. cp (H0 _ H3). bwi H4. eee.
  assert (Hb:forall i, inc i X -> target i = b).  ir. cp (H0 _ H3). bwi H4. eee.
  assert (Hd: forall i j, inc i X -> inc j X -> 
    agrees_on (intersection2 (source i) (source j)) i j).
  ir. cp (H0 _ H3). cp (H0 _ H4). bwi H5. bwi H6. ee.
  cp (H2 _ _ H3 H4). ufi gge H11. red. ee.
  app intersection2sub_first. app intersection2sub_second. 
  awii H11. ir. nin H11; ee. app W_extends. inter2tac. sy. app W_extends. 
  inter2tac. 
  assert (He:forall i, inc i X -> function_prop i (source i) b).
  ir. red. eee. 
  cp (extension_covering _ _ He Hd). nin H3. clear H4. nin H3. ee.
  red in H3. ee. assert (inc x (set_of_sub_functions a b)).
  bw. ee. am. rw H5. red. ir.
  nin (unionf_exists H7). nin H8. cp (H0 _ H8). bwi H10. eee. am.
  exists x. red. aw.   ee.  am. ir. aw.  ee. am. app H0. 
  cp (H0 _ H8). bwi H9. ee. 
  red. rw H11. rw H6. eee. rww sub_function. cp (H4 _ H8). 
  red in H12. red. eee. ir. sy. app H14. am. fprops.
Qed.


(** Full and short version of Zorn's lemma *)

Theorem Zorn_aux: forall r, order  r -> 
  (forall s, sub s (substrate r) -> worder (induced_order r s) ->
    (bounded_above r s)) -> 
  exists a, maximal_element r a.
Proof. ir. set ( px:= fun 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)).
  assert (forall X, inc X s -> px X (p X)). ir. ufi s H1. Ztac.  uf p.
  app choose_pr. 
  assert (sub s (powerset E)). uf s. app Z_sub.
  assert (forall x, inc x s -> (inc (p x) E & ~ (inc (p x) x))). 
  ir. cp (H1 _ H3). red in H4. ee.  red in H4. eee. am.
  cp (Zermelo_aux _  H2 H3). nin H4. ee. red in H4. ee.
  assert (Ha: order (induced_order r (substrate x))). fprops.
  assert (sub x (induced_order r (substrate x))). red. ir.
  assert (is_graph x). nin H4. fprops.  
  assert (J (P x0) (Q x0) = x0). cp (H10 _ H9). aw. wri H11 H9. wr H11.
  cp (inc_arg2_substrate H9).  nin (equal_or_not (P x0) (Q x0)). rw H13.
  order_tac. aw. assert (glt x (P x0) (Q x0)). red. au. 
  change (gle (induced_order r (substrate x)) (P x0) (Q x0)). aw.
  assert (inc (P x0) (segment x (Q x0))). rw segment_rw. am. am.
  cp (H7 _ H12).  cp (H8 _ H12). cp (H1 _ H16). red in H18. ee. red in H18.
  ee.  rwi H17 H20. cp (H20 _  H15). am.  substr_tac.
  assert (x = induced_order r  (substrate x)). ap extensionality. am. red. ir.
  assert (order (induced_order r (substrate x))). fprops.
  assert (is_graph (induced_order r (substrate x))). fprops.
  assert (J (P x0) (Q x0) = x0). cp(H12 _ H10). aw.  wr H13. wri H13 H10.
  cp (worder_total H4). assert (inc (P x0) (substrate x)). 
  cp (inc_arg1_substrate H10). awi H15. am. am. am.
  assert (inc (Q x0) (substrate x)).
  cp (inc_arg2_substrate H10). awi H16. am.  am. am. 
  nin (total_order_pr2 H14 H16 H15). nin H17.  red in H17. red in H17.
  cp (H9 _ H17).  elim H18.  order_tac. am.
  rwi H10 H4. cp (H0 _ H6 H4). red in H11. nin H11. red in H11. ee. 
  exists x0. red. ee. am. ir. nin (equal_or_not x0 x1). sy; am.
  assert (glt r x0 x1). split; am.
  elim H5. uf s. Ztac.  app powerset_inc. exists x1. red. ee. red. eee. 
  order_tac. ir. cp (H12 _ H16). order_tac. red. ir. cp (H12 _ H16). order_tac.
Qed.


Theorem Zorn_lemma: forall r, order  r -> inductive_set  r ->
  exists a, maximal_element r a.
Proof. ir. app Zorn_aux. ir. red in H0. red. app H0. app worder_total.
Qed.

(** Consequences *)

Lemma inductive_max_greater: forall r a, order r ->  inductive_set r ->
  inc a (substrate r) -> exists m, maximal_element r m & gle r a m.
Proof. ir. set (F:= Zo (substrate r)(fun z => gle r a z)).
  assert (sub F (substrate r)). uf F. app Z_sub.
  assert (order (induced_order r F)). fprops.
  assert (inc a F). uf F. Ztac. order_tac.
  assert (inductive_set (induced_order r F)). red. ir. awi H5.
  wri induced_trans H6. 
  red in H0. assert (sub (tack_on X a) (substrate r)). 
  red. ir. rwi tack_on_inc H7.  nin H7. app H2. app H5. rww H7.
  assert (order (induced_order r (tack_on X a))).  fprops.
  assert (total_order (induced_order r (tack_on X a))).  red.  eee. 
  aw. ir. awi H9. awi H10. uf gge. aw. 
  nin H9. nin H10. red in H6. ee. awi H11. nin (H11 _ _ H9 H10). awii H12.  
  au. red in H12. awii H12. au.  am. apw sub_trans F. cp (H5 _ H9). ufi F H11. 
  Ztac.  rw H10. au.  rw H9. nin H10. cp (H5 _ H10). ufi F H11. Ztac. au.
  rw H10. left. order_tac.
  nin (H0 _ H7 H9). red in H10. ee.
  assert (inc a (tack_on X a)). fprops. cp (H11 _ H12).
  assert (inc x F). uf F. Ztac. exists x. red. ee.
  aw. ir. aw.  assert (inc y  (tack_on X a)).  fprops. app H11. app H5. am.
  am. am. am. am. nin (Zorn_lemma H3 H5). exists x. red in H6. ee.
  red. ee.  awi H6. app H2. am. am. awi H6. ir.
  assert (inc x0 F). uf F. Ztac. order_tac. ufi F H6. Ztac. order_tac.
  app H7. aw. am.  am. awi H6.  ufi F H6. Ztac. am. am. am.
Qed.

Lemma inductive_powerset: forall 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_set (inclusion_suborder A).
Proof. ir. red. ir.  exists (union X). red. 
  assert (inc (union X) A). app H0. ir. red in H2.
  ee. awi H5. cp (H5 _ _ H3 H4). awi H6. nin H6.  ee. left. am. red in H6.
  awi H6. ee; right. am. am. am. am. am. fprops. am. awi H1. am.
  split. aw. ir. aw. awi H1. ee.  app H1. am. app union_sub.
Qed.

Lemma maximal_in_powerset: forall 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_element (inclusion_suborder A) a.
Proof. ir. assert (order (inclusion_suborder A)). fprops.
  cp (inductive_powerset H H0).  app  Zorn_lemma.
Qed.


Lemma minimal_in_powerset: forall A F, sub A (powerset F) -> nonempty A ->
  (forall So, (forall x y, inc x So -> inc y So -> sub x y \/ sub y x) ->
    sub So A -> inc (intersection So) A) ->
  exists a, minimal_element (inclusion_suborder A) a.
Proof. ir.  assert (order (inclusion_suborder A)). fprops. 
  assert (order ( opposite_order (inclusion_suborder A))). fprops. nin H0. 
  assert (inductive_set (opposite_order (inclusion_suborder A))).
  red. ir. nin (emptyset_dichot X).  exists y. red. ee. aw. ir.
  rwi H6 H7. elim (emptyset_pr H7).  exists (intersection X).  red. 
  assert (inc (intersection X) A). app H1. ir. red in H5. ee. awi H9. 
  cp (H9 _ _ H7 H8). ufi gge H10. awi H10. nin H10.  ee. right.  am. ee. 
  left. am. fprops. fprops. am. am. am. am. fprops.  aw. awi H4.  am. fprops. 
  awi H4. am.  fprops. aw. eee. ir. aw. eee. awi H4. app H4. fprops. 
  app intersection_sub.
  nin (Zorn_lemma H3 H4). rwi maximal_opposite H5. exists x. am. am.
Qed.

(** **  EIII-2-5  Isomorphisms of well-ordered sets *)

(** The next theorem essentially says that f is injective*)

Lemma order_morphism_pr1: forall f r r', 
  order r -> order r' -> is_function f -> substrate r = source f ->
  substrate r' = target f ->
  (forall x y, inc x (source f) -> inc y (source f) ->
    gle r x y = gle r' (W x f) (W y f))
  -> order_morphism f r r'.
Proof. ir. red. eee. red. eee. ir.
  assert (gle r' (W x f) (W x f)). order_tac. rw H3. app inc_W_target.
  ap (order_antisymmetry H (a:=x) (b:=y)); rww H4; wrr H7. 
Qed.

(** Uniqueness of morphism between segments of well-ordered sets *)

Lemma increasing_function_segments: forall r r' f g,
  worder r -> worder r' ->
  increasing_fun f r r' -> strict_increasing_fun g r r'->
  is_segment r' (range (graph f)) ->
  forall x, inc x (source f) -> gle r' (W x f) (W x g).
Proof. ir. red in H1. ee. destruct H2 as [Hfg [_ [ _ [ Hu [Hv Hx]]]]].
  set (s :=Zo (source f) (fun x => (glt r' (W x g) (W x f)))). 
  assert (source f = source g). ue. 
  cp (worder_total H). cp (worder_total H0).
  assert (inc (W x f) (substrate r')). rw H8. fprops.
  assert (inc (W x g) (substrate r')). rw Hv. rwi H2 H4. fprops.
  nin (total_order_pr2 H11 H13 H12); tv.
  assert (nonempty s).  exists x. uf s. Ztac. 
  assert (sub s (source f)). uf s. app Z_sub. 
  wri H7 H16. nin H. cp (H17 _ H16 H15). nin H18. red in H18. ee.
  awi H18. ufi s H18. Ztac. clear H18. red in H3. ee.
  assert (inc (W x0 f)  (range (graph f))). app inc_W_range_graph. 
  nin H21. cp (H18 _ _ H22 H21). awi H24. nin H24. assert (W x0 g = W x1 f). 
  sy. app (W_pr H1 H24). cp (inc_pr1graph_source H1 H24).
  assert (glt r' (W x1 f) (W x0 f)). wr H25. red; eee.
  assert (glt r x1 x0).  assert (glt r x1 x0 \/ gle r x0 x1).
  wri H7 H20; wri H7 H26. ap (total_order_pr2 H10 H26 H20). 
  nin H28. am.  cp (H9 _ _ H28). order_tac. 
  assert (inc (W x1 f) (substrate r')). rw H8. fprops. 
  assert (inc (W x1 g) (substrate r')). rw Hv. rwi H2 H26. fprops.
  nin (total_order_pr2 H11 H30 H29). assert (inc x1 s).
  uf s. Ztac. awi H19. cp (H19 _ H32).  cp (related_induced_order1 H33). 
  order_tac. am. am. cp (Hx _ _ H28). rwi H25 H32. order_tac. fprops. am. am. 
Qed.

Lemma isomorphism_worder_unique: forall r r' x y,
  worder r -> worder r' ->  is_segment r' (range (graph x)) ->
  is_segment r' (range (graph y)) -> 
  order_morphism x r r' -> order_morphism y r r'
  ->  x = y.
Proof. ir. cp (order_morphism_increasing H3). 
  cp (order_morphism_increasing H4).
  cp (increasing_fun_from_strict H5). cp (increasing_fun_from_strict H6).
  red in H3; red in H4. ee. app function_exten. red in H15; eee.
  red in H10; eee. wrr H16. wrr H17. ir. 
  cp (increasing_function_segments H H0  H7 H6 H1 H19).
  wri H16 H19. rwi H11 H19. cp (increasing_function_segments H H0 H8 H5 H2 H19).
  order_tac.
Qed.

Lemma induced_order_trans: forall a b c, sub c b -> 
  induced_order (induced_order a b) c = induced_order a c.
Proof. ir. uf induced_order.  assert (sub (coarse c) (coarse b)). uf coarse.
  app product_monotone. wr intersection2assoc. app uneq.
  rw intersection2comm. wrr intersection2_sub.
Qed.

Theorem isomorphism_worder: forall r r', worder r -> worder r' ->
  let iso:= (fun u v f => 
    is_segment v (range (graph f)) & order_morphism f u v) in
  exists_unique (fun f => iso r r' f) \/ exists_unique (fun f => iso r' r f).
Proof. ir.  set (E:= substrate r). set (E':= substrate r').
  assert (Ha: order r). nin H;am. 
  assert (Hb: order r'). nin H0; am.
  assert (Hy:order (extension_order E E')). fprops.
  assert (Hx:order (opposite_order (extension_order E E'))). fprops.
  assert (Hf: set_of_sub_functions E E' = 
    substrate (opposite_order (extension_order E E'))). aw. fprops.
  set (s:= (Zo (set_of_sub_functions E E')  (fun z  => exists u, 
    is_segment r u & iso (induced_order r u) r' z))).
  assert (Hu:sub s (set_of_sub_functions E E')). uf s. app Z_sub.  
  assert (Hp:sub s (substrate (opposite_order (extension_order E E')))). aw. 
  assert(inductive_set (induced_order(opposite_order(extension_order E E')) s)).
  red. aw. ir. rwii induced_order_trans H2. red in H2. awi H2. ee.
  assert (Hv:sub X (set_of_sub_functions E E')). app (sub_trans H1 Hu).
  assert (Hz:sub X (substrate (opposite_order (extension_order E E')))). aw. 
  assert (Hw:forall x, inc x s -> is_segment r (source x)).  ir. ufi s H4. 
  Ztac. nin H6. ee. red in H7. nin H7. nin H8. ee. wr H11. aw. app sub_segment1.
  assert (Ht:forall x, inc x s -> is_segment r' (range (graph x))). 
  ir. ufi s H4. Ztac. nin H6. ee. red in H7; ee. am.
  assert (forall u v x, inc u X -> inc v X ->  inc x (source u) -> 
    inc x (source v) ->   W x u = W x v).
  ir. cp (H3 _ _ H4 H5). ufi gge H8. awii H8. 
  nin H8 ; ee ; [ | sy]; app W_extends.  
  nin (sup_extension_order2 Hv H4). ee. awii H5. ee. red in H5. ee. wri Hf H5. 
  exists x.
  assert (Hs: inc x s).  uf s. Ztac. exists (source  x). 
  assert (Hc: is_segment r (source x)). rw H6. app unionf_is_segment. ir. 
  app Hw. app H1. ee. am. 
  assert(is_segment r' (range (graph x))). rw H7. app unionf_is_segment. ir. 
  app Ht. app H1. 
  red. ee. am.
  assert (sub (source x) (substrate r)).  red in Hc; eee.
  assert (sub (range (graph x)) (substrate r')).  red in H11; eee. 
  assert (forall a b,
    inc a (source x) ->  inc b (source x) ->
    gle (induced_order r (source  x)) a b =
    gle r' (W a x) (W b x)).
  ir. rwi H6 H14. rwi H6 H15. nin (unionf_exists H14). nin (unionf_exists H15). 
  ee.  assert (exists z,  inc z X & inc a (source z) & inc b (source z)).
  cp (H3 _ _  H16 H17). ufi gge H20. awii H20.
  nin H20; ee; cp (source_extends H22); [  exists x1 |  exists x0 ]; eee. 
  nin H20. clear H18; clear H19; clear H16; clear H17; ee.
  cp (H1 _ H16). ufi s H19. Ztac. clear H19. nin H21. ee.
  red in H21. nin H21. ee. red in H22. ee. awi H25. rwi H25 H27. 
  cp (H27 _ _ H17 H18). clear H27. awii H28. 
  cp (H10 _ H16). rwi (extension_order_pr H27 H17) H28. 
  rwi (extension_order_pr H27 H18) H28. wr H28. awi H27. ee.
  cp (source_extends H30). aw. app H31. app H31. fprops. am.
  app sub_segment1. bwi H5. ee.
  app  order_morphism_pr1; fprops. aw.  
  split. rww substrate_induced_order. 
  ir. cp (H10 _ H11). awii H12. aw. app H1. am. apw sub_trans s. aw. 
  assert (order (induced_order (opposite_order (extension_order E E')) s)).
  fprops.
  cp (Zorn_lemma H2 H1). clear H1. nin H3. red in H1. ee. awii H1. 
  awii H3. assert (Hm: inc x s). am. ufi s H1. Ztac. clear H1. nin H5. ee. 
  (* maybe x is the answer *) nin (equal_or_not x0 (substrate r)).
  rwi H6 H5. rwi induced_order_substrate H5. left. red. 
  ee. exists x. am. ir. red in H7; red in H8. nin H7. nin H8.
  ee. app (isomorphism_worder_unique (r:=r) (r':=r')).  am.
  (* maybe the inverse of x is the answer *)
  nin (equal_or_not (range (graph x))  (substrate r')). right. red. ee.
  bwi H4. ee. red in H5. ee.
  set (f:= corresp E' E (inverse_graph (graph x))). exists f. 
  assert (Hd: is_graph (graph x)). fprops. 
  assert (He: source x = x0).  red in H10. ee. awi H13. sy; am. am.
  app sub_segment1.
  assert (Hg: range (graph f) = x0). uf f. aw.  rww range_inverse.  aw.
  assert (is_function f). uf f. app is_function_pr. red. ee. fprops. 
  ir. rwii inverse_graph_rw H11. rwii inverse_graph_rw H12.
  ee. red in H10. ee. rwi H13 H15. cp (injective_pr3 H17 H15 H14).
  app pair_extensionality. ufi f Hg. awi Hg. rw Hg. ue.
  uf E'. wr H7. rww domain_inverse. red. split. ue.  
  app  order_morphism_pr1. uf f. aw. uf f. aw. ir.
  assert (forall u, inc u (source f) ->
    (inc (W u f) (source x) & W (W u f) x = u)).
  ir.  cp (W_pr3 H11 H14). set (v := W u f) in *.  ufi f H15. awi H15. 
  split. graph_tac. ap (W_pr H4 H15).  cp (H14 _ H12). cp (H14 _ H13). ee.
  set (a:=  (W x1 f)) in *. set (b:= (W y f)) in *. wr H18. wr H17. 
  red in H10. ee. wrr H23. aw. ue. ue.
  ir. red in H8; red in H9. ee.
  app (isomorphism_worder_unique (r:=r') (r':=r)).
  (* we construct an extension *)
  ir. nin (well_ordered_segment H H1).  elim H6. am. red in H5. ee.
  simpl in H5. nin (well_ordered_segment H0 H5). contradiction.
  nin H8. nin H10.
  set (f:=tack_on_f x x1 x2). red in H9. ee. awi H15.
  assert (Hq:is_function x).  fct_tac.
  assert (Ho:is_graph (graph x)).  fprops. 
  assert (Hn: is_graph (tack_on (graph x) (J x1 x2))). red. ir.  
  rwi tack_on_inc H18. nin H18. app Ho. rw H18. fprops. clear Hp.
  assert (Hp: ~ (inc x1 (source x))). wr H15. red. ir. 
  rwi H12 H18. elim (not_in_segment H18). 
  assert (is_function f). uf f. app tack_on_function. 
  assert (target f = E'). uf f. uf tack_on_f.  aw. wr H16. 
  uf E'. app tack_on_when_inc. 
  assert (source f = segment_c r x1). uf f. uf tack_on_f. aw.
  wr H15. rw H12. app segment_c_pr.
  assert (Hk: forall a, sub (segment_c r a) (substrate r)).
  ir. uf segment_c. uf interval_uc. app Z_sub. 
  assert (range (graph f) = segment_c r' x2). uf f. uf tack_on_f. aw.
  wr segment_c_pr. rw tack_on_range. ue. am. am.
  assert (inc f s). uf s. Ztac. bw. ee. am. rw H20. app Hk. am.
  exists (segment_c r x1). ee. app tack_on_segment. red. ee. 
  rw H21. app tack_on_segment.  app order_morphism_pr1.
  assert (sub (segment_c r x1) (substrate r)). app Hk. fprops.
  sy; aw. sy. am. ir.  transitivity (gle r x3 y). aw. ue. ue.
  wri segment_c_pr H20. wri H12 H20. rwi H15 H20. rwi H20 H22. rwi H20 H23.  
  awi H22. awi H23. uf f. nin H22. nin H23. rww tack_on_W_in. rww tack_on_W_in. 
  wrr  H17. aw. ue. ue. rw H23. rww tack_on_W_in. rww tack_on_W_out. 

 
  assert (inc  (W x3 x) (range (graph x))).
  app inc_W_range_graph. wri H15 H22. rwi H12 H22.  nin (inc_segment H22). 
  rwi H11 H24. nin (inc_segment H24). app iff_eq; ir; tv.  
  nin H23. rw H22. rww tack_on_W_out. rww tack_on_W_in. 
  assert (inc  (W y x) (range (graph x))).
  app inc_W_range_graph. wri H15 H23. rwi H12 H23.  cp (inc_segment H23). 
  rwi H11 H24. cp (inc_segment H24). app iff_eq; ir; order_tac.  
  rw H22; rw H23. rww tack_on_W_out. 
  assert (gle r x1 x1). wrr order_reflexivity. 
  assert (gle r' x2 x2). wrr order_reflexivity. app iff_eq; ir; tv.  am. am.
  assert (f = x). app H3. aw. bw. uf extends. bwi H4.  eee.  uf f.
  uf tack_on_f. aw. aw. fprops. ue. assert (inc x1 (source f)). rw H20.
  fprops. rwi H23 H24. contradiction. am. app sub_segment1.
Qed.

(** Consequences *) 

Lemma identity_isomorphism:  forall r, order r ->
  order_isomorphism (identity (substrate r)) r r.
Proof.  ir. red. eee. app identity_bijective. aw. aw. aw.
  ir. rw identity_W.  rw identity_W. tv. am. am.
Qed.
 
Lemma identity_morphism:  forall r, order r ->
  order_morphism (identity (substrate r)) r r.
Proof. ir. cp (identity_isomorphism H). red in H0. ee. red in H2. red. eee.
Qed.

Lemma unique_isomorphism_onto_segment: forall r f, worder r -> 
  is_segment r (range (graph f)) ->  order_morphism f r r ->
  f = identity (substrate r).
Proof. ir. assert (is_segment r (range (graph (identity (substrate r)))) &
    order_morphism (identity (substrate r)) r r). ee.
  assert (bijective (identity (substrate r))).  app identity_bijective. 
  nin H2. rw (surjective_pr3 H3). aw. app substrate_is_segment. 
  red in H;eee. app  identity_morphism. red in H; eee.
  nin (isomorphism_worder H H); nin H3; app H4; eee. 
Qed.

Lemma compose_order_isomorphism: forall r r' r'' f f',
  composable f' f -> order_isomorphism f r r' -> order_isomorphism f' r' r''
  -> order_isomorphism (compose f' f) r r''.
Proof. uf order_isomorphism. ir. eee. app compose_bijective. aw.  aw.
  ir. awi H12. awi H13. rww H11. assert (inc (W x f) (target f)).
  app inc_W_target.  app bij_is_function.
  assert (inc (W y f) (target f)).  app inc_W_target. app bij_is_function.
  aw. red in H. ee. wri H17 H14. wri H17 H15. rww  H6.  
Qed.

Lemma inverse_order_isomorphism: forall r r' f ,
   order_isomorphism f r r' -> order_isomorphism (inverse_fun f) r' r.
Proof. uf order_isomorphism. ir. eee. app inverse_bij_is_bij1. aw. aw. aw.
  ir. bwi H5. bwi H6.  set (x' := W x (inverse_fun f)).
  assert (x' = W x (inverse_fun f)). tv.  
   rw (W_inverse H1 H5 H7).
  set (y' := W y (inverse_fun f)).
  assert (y' = W y (inverse_fun f)). tv. rw (W_inverse H1 H6 H8). sy. 
  assert (source f = target (inverse_fun f)). aw.
  cp (inverse_bij_is_bij1 H1). nin H10. nin H10.
  app H4. rw H7; rw H9. app inc_W_target. aw.  rw H8; rw H9.
  app inc_W_target. aw.
Qed.

Lemma compose_order_morphism: forall r r' r'' f f',
  composable f' f -> order_morphism f r r' -> order_morphism f' r' r''
  -> order_morphism (compose f' f) r r''.
Proof. uf order_morphism. ir. eee. app compose_injective.   aw. aw. aw.
  ir. awi H12. awi H13. rww H11. assert (inc (W x f) (target f)).
  app inc_W_target. nin H8; am.
  assert (inc (W y f) (target f)).  app inc_W_target. nin H8; am.
  aw. red in H. ee. wri H17 H14. wri H17 H15. rww  H6.  
Qed.

Lemma bij_pair_isomorphism_onto_segment: forall r r' f f', 
  worder r -> worder r' -> 
  is_segment r' (range (graph f)) ->  order_morphism f r r' ->
  is_segment r (range (graph f')) ->  order_morphism f' r' r ->
  (order_isomorphism f r r' & order_isomorphism f' r' r & 
    f = inverse_fun f').
Proof. ir. cp H2. cp H4. red in H2. red in H4.
  set (goal:=order_isomorphism f r r' & order_isomorphism f' r' r 
    & f = inverse_fun f'). ee.
  assert (Ha:is_function f). nin H13; am.
  assert (Hb:is_function f'). nin H8; am.
  assert (is_graph (graph f)). fprops. assert (is_graph (graph f')). fprops.
  assert (composable f f'). red. eee. 
  assert (composable f' f). red. eee.
  cp (compose_order_morphism H19 H6 H5). cp (compose_order_morphism H20 H5 H6).
  assert (is_segment r (range (graph (compose f' f)))). red. ee.
  assert (target  (compose f' f) = substrate r). aw. sy. am. wr H23.
  red in H22. ee. red in H25; ee; red in H25. ee. fprops.  
  ir. ufi compose H23. awi H23. nin H23. awi H23. nin H23.  nin H25. nin H25. 
  red in H3. nin H3.
  red in H1. ee. assert (inc x1 (range (graph f))). ex_tac. 
  assert (inc x (range (graph f'))).  ex_tac. 
  cp (H27 _ _ H30 H24). awi H31. nin H31. cp (W_pr Hb H26). cp (W_pr Hb H31).
  wri H32 H24; wri H33 H24. wri H11 H24. cp (H28 _ _ H29 H24). awi H34. nin H34.
  aw. exists  x3. uf compose. aw. eee. 
  simpl. aw. exists x2. eee. uf compose. aw. fprops. fprops.
  graph_tac. graph_tac. am. fprops.
  assert (is_segment r' (range (graph (compose f f')))). red. ee.
  assert (target  (compose f f') = substrate r'). aw. sy. am. wr H24.
  red in H21. ee. red in H26; ee; red in H26; ee. fprops.
  ir. ufi compose  H24. awi H24. nin H24. awi H24. nin H24. nin H26. nin H26. 
  red in H3. nin H3.
  red in H1. ee. assert (inc x1 (range (graph f'))). ex_tac.
  assert (inc x (range (graph f))). ex_tac.
  cp (H29 _ _ H31 H25). awi H32. nin H32. cp (W_pr Ha H27). cp (W_pr Ha H32).
  wri H33 H25; wri H34 H25. wri H16 H25. cp (H28 _ _ H30 H25). awi H35. nin H35.
  uf compose. aw. exists  x3. aw. eee. exists x2. eee. fprops. am.
  graph_tac. graph_tac.  fprops. 
  fprops. cp (unique_isomorphism_onto_segment H H23 H22).
  cp (unique_isomorphism_onto_segment H0 H24 H21).
  rwi H9 H26. rwi H14 H25.  cp (bijective_from_compose H19 H20 H26 H25).
  uf goal. ee. red. eee. ee. red. eee. am.
Qed.

Lemma isomorphic_subset_segment: forall r a,
  worder r -> sub a (substrate r) -> 
  exists w, exists f, is_segment r w &  
    order_isomorphism f (induced_order r a) (induced_order r w).
Proof. ir. cp (worder_restriction H H0). cp (isomorphism_worder H1 H).
  nin H2. nin H2. nin H2. clear H3. ee. nin H.
  exists (range (graph x)).
  assert (Hz: a = source x). red in H3. ee. wr H7. aw. red in H3. ee. nin H6.
  assert (Hw: transf_axioms (fun z => W z x) (source x) (range (graph x))). 
  red. ir. app inc_W_range_graph. 
  assert (He: is_graph (graph x)). fprops.
  assert (Hd:sub (range (graph x)) (substrate r)). red in H2. eee.   
  set (f := BL (fun z => W z x) (source x) (range (graph x))). exists f. eee.
  red. uf f. aw. eee. app bl_bijective. ir. awi H11.  nin H11. exists x0.
  ee.  graph_tac.  graph_tac. am. 
  ir. rww H9. aw. exists x0. app W_pr3. exists y. app W_pr3.

  nin H2. clear H3. nin H2. nin H2. nin (well_ordered_segment H1 H2).
  red in H3. ee.
  ir. assert (order_isomorphism x r (induced_order r a)). red. eee.
  red. ee. am. app surjective_pr4. red in H6. ee. am. rw H4. am.
  cp (inverse_order_isomorphism H10). exists (substrate r). 
  exists (inverse_fun x). ee. app substrate_is_segment. 
  rw induced_order_substrate. am. fprops. 

  nin H4. red in H3. ee. awii H4. assert (inc x0 (substrate r)). app H0.
  assert (inc (W x0 x) (segment  (induced_order r a) x0)). wr H5. 
  app inc_W_range_graph. fct_tac. wrr H8. 
  set (s :=Zo (source x) (fun a => (glt r (W a x) a))). 
  assert (nonempty s).  exists x0. uf s. Ztac. wrr H8. 
  cp (inc_segment H12). app (related_induced_order2 H13).
  assert (sub s (source x)). uf s. app Z_sub. red in H. ee. 
  wri H8 H14. cp (H15 _ H14 H13). nin H16. red in H16. awii H16. ee.
  ufi s H16. Ztac. clear H16.
  assert (inc (W x1 x) s).  uf s.
  assert (inc (W x1 x) (source x)). wr H8. order_tac. nin H19. 
  rwi (H10 _ _ H16 H18) H19. set (related_induced_order1 H19).
  Ztac. split. aw. dneg. nin H7.  app H22. 
  set (related_induced_order1  (H17 _ H16)). order_tac.
Qed.

(** **  EIII-2-6  Lexicographic Products *)

Definition lexicographic_order_r (r g:Set): EEP := 
  fun x x' => 
    forall j, least_element (induced_order r (Zo (domain g)
      (fun i =>  V i x <> V i x'))) j -> glt (V j g) (V j x)(V j x').

Definition lexicographic_order_axioms r g:=
  worder r & substrate r = domain g & fgraph g & 
  (forall i, inc i (domain g) -> order (V i g)).

Definition lexicographic_order r g := 
  graph_on (lexicographic_order_r r g)(prod_of_substrates g).


Lemma lexorder_substrate_aux: forall r g x,
  lexicographic_order_axioms r g ->
  lexicographic_order_r r g x x.
Proof. ir. red in H. ee. red. ir. red in H3. awi H3. ee. Ztac.  
  elim H6. tv. nin H; am. rw H0. app Z_sub.
Qed.

Lemma lexorder_substrate: forall r g,
  lexicographic_order_axioms r g ->
  substrate(lexicographic_order r g) = prod_of_substrates g.
Proof. ir. uf lexicographic_order. rww substrate_graph_on. ir.
  app lexorder_substrate_aux.
Qed.

Hint Rewrite lexorder_substrate : bw.

Lemma lexorder_order: forall r g,
  lexicographic_order_axioms r g -> order (lexicographic_order r g).
Proof. ir. assert (Hww:= H). red in H. ee. 
  assert (Ha: total_order r). app worder_total.  nin H.
  uf lexicographic_order. app order_from_rel1. red. 
  ir. uf lexicographic_order_r.  ir.
  set (s:= Zo (substrate r) (fun i => (V i x <> V i y) \/ (V i y <> V i z)
    \/  V i x <> V i z)). red in H6. wri H0 H6. awii H6; try app Z_sub. nin H6. 
  assert (inc j s). Ztac. clear H6. uf s. Ztac. 
  assert (sub s (substrate r)). uf s. app Z_sub. 
  assert (nonempty s). ex_tac. nin (H3 _ H9 H10). red in H11. awii H11. 
  nin H11. ufi s H11. Ztac. clear H11.
  nin (equal_or_not (V x0 x) (V x0 y)). 
  assert (V x0 y <> V x0 z). nin H14. contradiction. nin H14. am. ue.
  assert (x0 = j).  cp (H12 _ H8). cp (related_induced_order1 H16). clear H16.
  assert (inc x0 (Zo (substrate r) (fun i => V i x <> V i z))).  Ztac. ue.
  cp (H7 _ H16).  cp (related_induced_order1 H18). order_tac.
  assert (least_element (induced_order r (Zo (substrate r) 
    (fun i => V i y <> V i z))) j). 
  red. aw. ee. Ztac. ue. ir. Ztac. clear H17. aw.
  wr H16. assert (inc x1 s). uf s. Ztac. cp (H12 _ H17).
  ap (related_induced_order1 H20).  Ztac. ue. Ztac. app Z_sub.
  rwi H0 H17. cp (H5 _ H17). wri H16 H18. wri H11 H18. wrr H16. 
  nin (equal_or_not (V x0 y) (V x0 z)). 
  assert (x0 = j). cp (H12 _ H8). cp (related_induced_order1 H16). 
  assert (inc x0 (Zo (substrate r) (fun i => V i x <> V i z))).  Ztac.
  wrr H15. cp (H7 _ H18). cp (related_induced_order1 H19). order_tac.
  assert (least_element (induced_order r (Zo (substrate r) 
    (fun i => V i x <> V i y))) j). 
  red. aw. ee. Ztac. ue. ir. Ztac. clear H17. aw.
  wr H16. assert (inc x1 s). uf s. Ztac. cp (H12 _ H17).
  ap (related_induced_order1 H20). Ztac. ue. Ztac. app Z_sub.
  rwi H0 H17. rwi H16 H15. wr H15. app (H4 _ H17).
  assert (least_element (induced_order r (Zo (substrate r) 
  (fun i => V i x <> V i y))) x0). 
  red. aw. ee. Ztac. ir. Ztac. clear H16. aw. assert (inc x1 s). uf s. 
  Ztac. cp (H12 _ H16). ap (related_induced_order1 H19). Ztac. Ztac. app Z_sub.
  rwi H0 H16. cp (H4 _ H16). 
  assert (least_element (induced_order r (Zo (substrate r) 
  (fun i => V i y <> V i z))) x0). 
  red. aw. ee. Ztac. ir. Ztac. clear H18. aw. assert (inc x1 s). uf s. 
  Ztac. cp (H12 _ H18). ap (related_induced_order1 H21). Ztac. Ztac. app Z_sub.
  rwi H0 H18. cp (H5 _ H18). assert (glt (V x0 g) (V x0 x) (V x0 z)). 
  rwi H0 H13. cp (H2 _ H13). nin H19. order_tac.
  assert (x0 = j). cp (H12 _ H8). cp (related_induced_order1 H21). 
  assert (inc x0 (Zo (substrate r) (fun i => V i x <> V i z))).  Ztac.
  nin H20; am. cp (H7 _ H23). cp (related_induced_order1 H24). 
  order_tac. ue. 
  ir.  set (s:=(Zo (domain g) (fun i : Set => V i u <> V i v))).
  nin (emptyset_dichot s). ufi product_order H4. 
  ufi prod_of_substrates H4.  ufi prod_of_substrates H5. 
  assert (fgraph  (fam_of_substrates g)). uf fam_of_substrates. gprops.
  app (productb_exten H9 H4 H5). ir. ufi fam_of_substrates H10. bwi H10.
  ex_middle. assert (inc i emptyset).
  wr H8. uf s.  Ztac. elim (emptyset_pr H12). 
  assert (s=(Zo (domain g) (fun i : Set => V i v <> V i u))). 
  uf s. set_extens; Ztac.
  assert (sub s (substrate r)). uf s. rw H0. app Z_sub.
  cp (H3 _ H10 H8). nin H11. cp (H6 _ H11).  rwi H9 H11. nin (H7 _ H11). 
  assert (inc x (domain g)). red in H11. nin H11. awi H11. Ztac. am. am.
  rw H0. app Z_sub.  cp (H2 _ H15).   order_tac.
  ir. app lexorder_substrate_aux.
Qed.

Lemma lexorder_gle: forall r g x x',
  lexicographic_order_axioms r g -> 
  related (lexicographic_order r g) x x' = 
  (inc x (prod_of_substrates g)&  inc x' (prod_of_substrates g) &
    forall j, least_element (induced_order r (Zo (domain g)
      (fun i =>  V i x <> V i x'))) j -> glt (V j g) (V j x)(V j x')).
Proof. ir. uf lexicographic_order. rww graph_on_rw1. 
Qed.

Hint Resolve lexorder_order: fprops.
Hint Rewrite lexorder_gle : aw.

Lemma lexorder_total: forall r g,
  lexicographic_order_axioms r g ->
  (forall i, inc i (domain g) -> total_order (V i g)) ->
  total_order (lexicographic_order r g).
Proof. ir. red.  assert (Hb:= H). assert (Hc:order (lexicographic_order r g)).
  fprops. ee. am. bw. ir. 
  assert (Hd:fgraph (fam_of_substrates g)). uf fam_of_substrates. gprops.
  set (s:=(Zo (substrate r) (fun i : Set => V i x <> V i y))).
  nin (emptyset_dichot s).  assert (x = y). red in H. ee.
  ufi prod_of_substrates H1.   ufi prod_of_substrates H2.
  ap (productb_exten Hd H1 H2). ir. 
  nin (p_or_not_p (V i x = V i y)).  am.  empty_tac1 i.
  uf s. Ztac. ufi fam_of_substrates H7. bwi H7. ue. 
  left. rw H4. order_tac. bw.
  assert (sub s (substrate r)). uf s; app Z_sub. nin H. nin H. 
  nin (H6 _ H4 H3).  assert (Ha:= H7).
  red in H7. awi H7. ee. assert (inc x0 (domain g)). wr H5. app H4.
  nin (H0 _ H11).  ufi s H5. Ztac.  clear H5.
  assert (inc (V x0 x) (substrate (V x0 g))). ufi prod_of_substrates H1. 
  ufi fam_of_substrates H1.  awi H1. ee. bwi H5.
  rwi H5 H14. cp (H14 _ H11). bwi H15. am. am. gprops.
  assert (inc (V x0 y) (substrate (V x0 g))).  ufi prod_of_substrates H2. 
  ufi fam_of_substrates H2. awi H2. ee. bwi H14.
  rwi H14 H15. cp (H15 _ H11). bwi H16. am. am. gprops. 
  assert (Ht: product_order_axioms g). red. eee.
  assert (fgraph (fam_of_substrates g)). uf fam_of_substrates. gprops.
  assert (domain (fam_of_substrates g) = domain g). uf fam_of_substrates. bw.
  ufi prod_of_substrates H1.  ufi prod_of_substrates H2. awii H1. awii H2. 
  ufi fam_of_substrates H1. bwi H1.  ufi fam_of_substrates H2. bwi H2. ee.
  nin (H13 _ _ H5 H14).  left. 
  aw. eee. ir. wri H19 H22. wri H19 H20. cp (H20 _ H22). bwi H23. am. am.
  ir. wri H17 H22. cp (H18 _ H22). bwi H23. am. ue. ir.
  assert (order (induced_order r s)). fprops. fold s in H22.
  red in Hb. ee. wri H25 H22. fold s in H22.  rw (unique_least H23 H22 Ha).
  red; ee. am. ufi s H7.  Ztac. am. red in Hb; ee.
  right. red.  aw. eee. ir. wri H23 H18.  wri H17 H26. cp (H18 _ H26). 
  bwi H27. am. ue. ue.
  ir. wri H19 H26. cp (H20 _ H26). bwi H27. am. ue. ir.
  assert (s =  (Zo (domain g) (fun i : Set => V i y <> V i x))).
  uf s. rw H23. set_extens; Ztac. wri H27 H26.
  assert (order (induced_order r s)). fprops. rw (unique_least H28 H26 Ha).
  red; ee. am. ufi s H7.  Ztac. int. red. eee. am. uf s. app Z_sub.
Qed.

(** ** Ordinals *)



Lemma disjoint_union2_rw:  forall a b x y,  y <> x ->
  disjoint_union (variantL x y a b) =
  union2 (product a (singleton x)) (product b (singleton y)).
Proof. ir. uf disjoint_union. uf disjoint_union_fam.
  assert (Ha: domain (variantL x y a b) = doubleton x y). uf variantL. bw.
  set_extens. rwi unionb_rw H0. nin H0. ee. bwi H0. bwi H1. rwi Ha H0.
  nin (doubleton_or H0). rwi H2 H1. rwi variant_V_a H1. inter2tac.
  rwi H2 H1. rwi variant_V_b H1. inter2tac. am. am. 
  rw unionb_rw.  bw. nin (union2_or H0). exists x. ee. rw Ha. fprops. bw.
  rw variant_V_a. am. rw Ha. fprops. exists y. rw Ha. eee. bw. 
  rww variant_V_b. fprops.
Qed.

Lemma disjoint_union2_rw1:  forall a b,
  disjoint_union (variantLc a b) =
  union2 (product a (singleton TPa)) (product b (singleton TPb)).
Proof. ir. uf variantLc. rw disjoint_union2_rw. tv. fprops.
Qed.


End Worder.
Export Worder.