Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset6.


Import Correspondence.
Import Bfunction.
Import Border.
Import Worder.

Module Bordinal.

Lemma orderIR: forall r,
  order r -> r \Is r.
Proof.
move=> r or; exists (identity (substrate r)).
red;ee; aw.
  apply identity_bijective.
move=> x y xsr ysr; rewrite ! identity_W //.
Qed.

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

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

Lemma order_isomorphism_morphism: forall r r' f,
   order_isomorphism f r r' -> order_morphism f r r'.
Proof.
move=> r r' f; rewrite /order_isomorphism /order_morphism.
move=> [pa [pb [[pc _] [pd [pe pf]]]]]; ee.
Qed.

Lemma order_morphism_pr1: forall r r' f a b,
  order_morphism f r r' -> inc a (source f) -> inc b (source f) ->
  (glt r a b = glt r' (W a f) (W b f)).
Proof.
move=> r r' f a b or asf bsf.
move: or =>[or [or' [bf [sf [tf mp]]]]].
rewrite /glt (mp _ _ asf bsf); apply iff_eq;move=> [hle hne]; ee; dneg sw.
  move: bf => [_ injf]; apply injf =>//.
rewrite sw //.
Qed.

Lemma order_isomorphism_pr1: forall r r' f a b,
  order_isomorphism f r r' -> inc a (source f) -> inc b (source f) ->
  (glt r a b = glt r' (W a f) (W b f)).
Proof.
move=> r r' f a b or asf bsf.
by apply order_morphism_pr1 => //; apply order_isomorphism_morphism.
Qed.

Lemma order_morphism_pr0: forall r r' f a b,
  order_morphism f r r' -> inc a (substrate r) -> inc b (substrate r) ->
  (glt r a b = glt r' (W a f) (W b f)).
Proof.
move=> r r' f a b or asr bsr.
have sr: (substrate r = source f) by move: or =>[_ [_ [_ [sf _]]]].
rewrite sr in asr bsr; apply order_morphism_pr1=> //.
Qed.

Lemma order_isomorphism_pr0: forall r r' f a b,
  order_isomorphism f r r' -> inc a (substrate r) -> inc b (substrate r) ->
  (glt r a b = glt r' (W a f) (W b f)).
Proof.
move=> r r' f a b or asr bsr.
by apply order_morphism_pr0 => //; apply order_isomorphism_morphism.
Qed.

Lemma order_morphism_pr2: forall r r' f a b,
  order_morphism f r r' -> glt r a b ->
  glt r' (W a f) (W b f).
Proof.
move=> r r' f a b or ltab.
have asr: (inc a (substrate r)) by order_tac.
have bsr: (inc b (substrate r)) by order_tac.
rewrite -(order_morphism_pr0 or asr bsr) //.
Qed.

Lemma order_isomorphism_pr2: forall r r' f a b,
  order_isomorphism f r r' -> glt r a b ->
  glt r' (W a f) (W b f).
Proof.
move=> r r' f a b or ltab.
apply (order_morphism_pr2 (order_isomorphism_morphism or) ltab).
Qed.

Lemma total_order_morphism: forall f r r',
  total_order r -> order r' ->
  injection 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.
move=> f r r' to or' [ff injf] sf tf incf.
apply total_order_increasing_morphism => //.
move: to => [or _]; red; ee.
move=> x y [lexy nxy].
have xsf:inc x (source f) by rewrite -sf; order_tac.
have ysf:inc y (source f) by rewrite -sf; order_tac.
by split; [apply incf | dneg aa; apply injf].
Qed.

Lemma total_order_isomorphism: forall f r r',
  total_order r -> order r' ->
  bijection 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_isomorphism f r r'.
Proof.
move=> f r r' to or' bjf sf tf incf.
move: (bjf) => [injf _].
have: (order_morphism f r r') by apply total_order_morphism.
rewrite /order_morphism /order_isomorphism; intuition.
Qed.

Lemma segments_iso1: forall a A B, worder a -> sub A B ->
  is_segment a A -> is_segment a B ->
  (induced_order a B) \Is (induced_order a A) -> A = B.
Proof.
move => a A B woa AB sA sB oi.
move: oi => [f [ora [orb [[[ff injf] sjf] [sf [tf isf]]]]]].
have oa: order a by move: woa => [o _].
have As: sub A (substrate a) by apply sub_segment1.
have Bs: sub B (substrate a) by apply sub_segment1.
move: sf tf; aw=> sf tf.
rewrite -sf in injf isf.
have ta: transf_axioms (fun z => W z f) B B.
    move=> t tx; apply AB; rewrite tf;apply inc_W_target =>//; ue.
set g := BL (fun z => W z f) B B.
have fg: is_function g by apply bl_function.
have rg: (range (graph g) = A).
  rewrite tf;set_extens t; rewrite range_inc_rw //.
  move=> [u []]; rewrite /g => uc; awi uc; aw.
    move => ->; apply inc_W_target =>//; ue.
  move=> tif; move: (surjective_pr2 sjf tif) => [u [usf]].
 rewrite -sf in usf;move=> <-; exists u; rewrite /g; aw; ee.
have sr: is_segment (induced_order a B) (range (graph g)).
  rewrite rg; red; aw;split => //.
  move => x y xA leyx; move: (iorder_gle1 leyx).
  move: sA xA; rewrite /is_segment; move=>[_]; apply.
have om: order_morphism g (induced_order a B)(induced_order a B).
  red; ee; rewrite /g; aw.
    apply bl_injective => //.
  move=> x y xB yB. rewrite bl_W // bl_W //.
  move: (isf _ _ xB yB).
  aw; try apply ta =>//; rewrite tf; apply inc_W_target =>//; ue.
move: (worder_restriction woa Bs) => wob.
move: (unique_isomorphism_onto_segment wob sr om) => gi.
symmetry;move: rg; rewrite gi; aw; rewrite surjective_pr3 //; aw.
by move: (identity_bijective B) => [_ ok].
Qed.

Lemma segments_iso2: forall a A B, worder a ->
   inc A (set_of_segments a) -> inc B (set_of_segments a) ->
   (induced_order a A) \Is (induced_order a B) -> A = B.
Proof.
move=> a A B woa As Bs.
move: (worder_total (set_of_segments_worder woa)) => [or tor].
awi tor; move: (tor _ _ As Bs); rewrite /gge; aw.
rewrite -inc_set_of_segments// in As.
rewrite -inc_set_of_segments// in Bs.
case; last by move=> [_ [_ sAB]] oi; symmetry; apply (segments_iso1 woa)=>//.
move=> [_ [_ sAB]] oi; move: (orderIS oi) => oi'.
apply (segments_iso1 woa)=>//.
Qed.

Lemma isomorphism_worder2: forall r r', worder r -> worder r' ->
  r \Is r'
  \/ (exists x, inc x (substrate r) &
    (induced_order r (segment r x)) \Is r')
  \/ (exists x', inc x' (substrate r') &
   (induced_order r' (segment r' x')) \Is r).
Proof.
move => r r' wor wor'.
case: (isomorphism_worder wor wor'); move=> [[f [fp1 fp2]] _].
  move: fp2 => [pa [pb [pc [pd [pe pf]]]]].
  have ff: is_function f by fct_tac.
  case : (well_ordered_segment wor' fp1) => eq1.
    left;exists f; red; ee.
    split =>//; apply surjective_pr4 => //;apply extensionality.
      fct_tac.
    rewrite eq1 pe; fprops.
  move: eq1 => [x [xsr' rgx]].
  right; right; ee; ex_tac; apply orderIS.
  move: (@sub_segment r' x) => p1.
  exists (restriction1 f (source f)); red; ee.
    apply restriction1_bijective => //.
    rewrite /restriction1; aw.
    rewrite /restriction1; aw; rewrite image_by_fun_source // rgx.
  rewrite {1 2} /restriction1; aw. move=> a b ax bx.
  move: (@sub_refl (source f)) => ssf.
  rewrite (restriction1_W ff ssf ax) (restriction1_W ff ssf bx).
  aw; try (apply pf => //); rewrite -rgx; apply inc_W_range_graph => //.
move: fp2 => [pa [pb [pc [pd [pe pf]]]]].
have ff: is_function f by fct_tac.
case : (well_ordered_segment wor fp1) => eq1.
  left;apply orderIS; exists f; red; ee.
    split =>//; apply surjective_pr4 => //;apply extensionality.
      fct_tac.
    rewrite eq1 pe; fprops.
move: eq1 => [x [xsr rgx]].
right; left; ee; ex_tac; apply orderIS.
move: (@sub_segment r x) => p1.
exists (restriction1 f (source f)); red; ee.
  apply restriction1_bijective => //.
  rewrite /restriction1; aw.
  rewrite /restriction1; aw; rewrite image_by_fun_source // rgx.
rewrite {1 2} /restriction1; aw. move=> a b ax bx.
move: (@sub_refl (source f)) => ssf.
rewrite (restriction1_W ff ssf ax) (restriction1_W ff ssf bx).
aw; try (apply pf => //); rewrite -rgx; apply inc_W_range_graph => //.
Qed.

Lemma order_le_alt: forall r r',
   order r -> order r' ->
   (exists f, order_morphism f r r')
  -> (exists f, exists x, sub x (substrate r') &
       order_isomorphism f r (induced_order r' x)).
Proof.
move => r r' or or' [f [oa [oc [injf [sf [tf isof]]]]]].
set g := restriction1 f (source f).
have aux: sub (source f) (source f) by fprops.
have bg:bijection g by rewrite /g; apply restriction1_bijective =>//.
set X:= target g.
have ff: is_function f by fct_tac.
have Xs: sub X (substrate r').
  move => t; rewrite /X /g/restriction1; aw; fprops.
  move=> [u [usf]] <-; rewrite tf; fprops.
have sg: source g = source f by rewrite /g/restriction1; aw.
exists g; exists X;ee;red; rewrite -/X sg;ee; first by aw.
move=> x y xsf ysf; rewrite /g restriction1_W // restriction1_W //.
have p1: inc (W x f) X by rewrite /X/g/restriction1; aw; clear ysf; ex_tac.
have p2: inc (W y f) X by rewrite /X/g/restriction1; aw; ex_tac.
aw; apply isof => //.
Qed.

Lemma order_le_alt2: forall f a b x, order a -> order b ->
  sub x (substrate b) ->
  let F := (BL (fun z => W z f) (substrate a) (substrate b)) in
    order_isomorphism f a (induced_order b x)
    -> (order_morphism F a b & range (graph F) = x).
Proof.
move=> h u v x oa ob sxa F [ou [ov' [iz [sz [tz siz]]]]].
awi tz => //.
have fh: is_function h by fct_tac.
have ta1: transf_axioms (fun z => W z h) (substrate u) (substrate v).
  move=> t tu; apply sxa; rewrite tz; apply inc_W_target =>//;ue.
have fF: is_function F by apply bl_function.
have rg: range (graph F) = x.
    have gF:is_graph (graph F) by fprops.
    rewrite tz ;set_extens w; dw.
      move => [x0 Jg]; move: (inc_pr1graph_source fF Jg); rewrite /F; aw.
      move=> x0s; move: (W_pr fF Jg); rewrite /F; aw.
         move => <-; apply inc_W_target =>//; ue.
    move=> wt;move: iz =>[_ sjh]; move: (surjective_pr2 sjh wt) => [x0 [xs]] <-. exists x0.
    have ->: W x0 h = W x0 F by rewrite /F; aw; ue.
    apply W_pr3 =>//; rewrite /F; aw; ue.
split =>//.
  rewrite /F;red; ee; aw.
    apply bl_injective =>//; move=> x1 x2 x1s x2s.
    by move: iz =>[[_ ih] _]; rewrite -sz in ih; apply ih.
  move=> x1 x2 x1s x2s; aw; rewrite -sz in siz; rewrite siz //; aw.
    rewrite tz; apply inc_W_target=>//; ue.
  rewrite tz; apply inc_W_target=>//; ue.
Qed.

Lemma tack_on_injective_card1: forall x y a b,
  ~ (inc a x) -> ~ (inc b y) ->
  (tack_on x a) \Eq (tack_on y b) -> x \Eq y.
Proof.
move=> x y A B nax nby [f [[[ff injf] sjf] [sf tf]]].
have yt: inc B (target f) by rewrite tf; fprops.
move: (surjective_pr2 sjf yt) => [a [asf Wa]].
set g := BL (fun b => Yo (b = a) (W A f) (W b f)) x y.
exists g; rewrite /g;ee; aw.
have xsf: inc A (source f) by rewrite sf; fprops.
have sxsf: sub x (source f) by rewrite sf; move=> t; fprops.
apply bl_bijective.
    move=> b bx; simpl; Ytac ba.
      move: (inc_W_target ff xsf); rewrite tf; aw.
      case; first by intuition.
      move=> h; rewrite -h in Wa; move: (injf _ _ asf xsf Wa).
      move=> ax; rewrite ba ax in bx; contradiction.
    have bsf: inc b (source f) by rewrite sf; fprops.
    move: (inc_W_target ff bsf); rewrite tf; aw.
    case; first by intuition.
    move=> h; rewrite -h in Wa; move: (injf _ _ asf bsf Wa).
    move=> ab; elim ba; intuition.
  move=> u v ux vx; Ytac ua.
    Ytac va; first by rewrite ua va.
    move=> WW; move: (injf _ _ xsf (sxsf _ vx) WW) => aux.
    rewrite -aux in vx; contradiction.
  Ytac va; last by move=> ww;apply (injf _ _ (sxsf _ ux) (sxsf _ vx) ww).
    move=> WW;move: (injf _ _ (sxsf _ ux) xsf WW) => aux.
  by elim nax; rewrite -aux.
move=> z zt.
have ztf: (inc z (target f)) by rewrite tf ;fprops.
case (equal_or_not z (W A f)) => zW.
  rewrite zW; exists a; rewrite Y_if_rw; ee.
  move: asf; rewrite sf; aw; case => //.
  move=> ax;move: zt; rewrite zW -{1} ax Wa => nyy; contradiction.
move: (surjective_pr2 sjf ztf) => [b [bsf Wb]].
exists b; Ytac ba; first by elim nby; move: zt; rewrite -/y -Wb ba Wa.
ee; move: bsf; rewrite sf; aw; case=>// bx.
by elim zW; rewrite -Wb bx.
Qed.

Lemma tack_on_injective_card2: forall x y a b,
  ~ (inc a x) -> ~ (inc b y) ->
   (tack_on x a) \Eq (tack_on y b) = x \Eq y.
Proof.
move=> x y a b ax bx; apply iff_eq; first by apply tack_on_injective_card1.
move=> [f [ [[ff injf] srjf] [sf tf]]].
have sjt: surjection (tack_on_f f a b) by apply tack_on_surjective =>//;ue.
have st: source (tack_on_f f a b) = tack_on x a by rewrite /tack_on_f; aw;ue.
have tt: target (tack_on_f f a b) = tack_on y b by rewrite /tack_on_f; aw;ue.
have asf: ~ inc a (source f) by ue.
exists (tack_on_f f a b); ee.
split; ee; split; first by fct_tac.
rewrite st; move=> u v; aw; case => us; case=> vs.
      rewrite ! tack_on_W_in //; try ue; apply injf; ue.
    rewrite tack_on_W_in //; last by ue.
    rewrite vs tack_on_W_out //; move =>h; elim bx; rewrite -h.
    rewrite -tf; apply inc_W_target => //; ue.
  rewrite us tack_on_W_out // tack_on_W_in //; last by ue.
   move =>h; elim bx; rewrite h.
   rewrite -tf; apply inc_W_target => //; ue.
rewrite us vs !tack_on_W_out //.
Qed.

Lemma tack_on_injective_card3: forall x y a b,
  ~ (inc a x) -> ~ (inc b y) ->
  sub x y -> x \Eq (tack_on x a) ->
  y \Eq (tack_on y b).
Proof.
move=> x y A B Ab By sxy aux.
have nbx: ~ inc B x by dneg bx; apply sxy.
move: (equipotent_symmetric aux)=> [f [[[ff injf] sjf] [sf tf]]].
eqsym; clear aux.
have Asf: inc A (source f) by rewrite sf; fprops.
have wafx: inc (W A f) x.
  by rewrite -tf; apply inc_W_target =>//.
set g := fun z => Yo (inc z x) (W z f) (Yo (z = B) (W A f) z).
have Byp: forall t, inc t y -> t <> B by move=> t ty tB; elim By; ue.
exists (BL g (tack_on y B) y); aw; ee; apply bl_bijective.
    move=> t; aw; rewrite /g; case.
      move=> ty; Ytac1 tx.
        apply sxy;rewrite -tf;apply inc_W_target => //; rewrite sf; fprops.
      by move: (Byp _ ty) => aux; Ytac0.
    by move => ->; Ytac0; Ytac0; apply sxy.
  move=> u v; aw;rewrite /g; case => uy aux.
    Ytac1 ux.
       Ytac1 vx; first by apply injf; rewrite sf; fprops.
       case: aux => vy.
          move: (Byp _ vy) => aux; Ytac0=> h; elim vx; rewrite -h -tf.
         apply inc_W_target => //; rewrite sf; fprops.
      Ytac0 => aux.
      have usf: inc u (source f) by rewrite sf; fprops.
      rewrite (injf _ _ usf Asf aux) in ux; contradiction.
    have uB: u <> B by move => ub; elim By; ue.
    Ytac0; Ytac1 vx.
      move=> h; rewrite h in ux; elim ux; rewrite -tf.
      apply inc_W_target => //; rewrite sf; fprops.
    case: aux => vy; [move: (Byp _ vy) => aux |]; Ytac0 => //.
    move=> h;elim ux; ue.
  rewrite uy; Ytac0; Ytac0; Ytac1 vx.
     have vsf: inc v (source f) by rewrite sf; fprops.
     move=> h; rewrite -(injf _ _ Asf vsf h) in vx; contradiction.
  case:aux => vy => //.
  move: (Byp _ vy) => aux;Ytac0 => h; rewrite -h in vx; contradiction.
move=> t ty.
case (inc_or_not t x) => tx.
  rewrite -tf in tx; move: (surjective_pr2 sjf tx)=> [z [zsf wz]].
  move: zsf; rewrite sf; aw; case => zx.
    exists z; rewrite /g; Ytac0; ee.
  exists B; rewrite /g; Ytac0; Ytac0; ee; ue.
move: (Byp _ ty) => aux;exists t; rewrite /g; Ytac0; Ytac0; ee.
Qed.

Lemma Cantor_Bernstein1: forall E F f,
  sub F E ->
  (forall x, inc x E -> inc (f x) F) ->
  (forall x y, inc x E -> inc y E -> f x = f y -> x = y) ->
  E \Eq F.
Proof.
move=> E F f FE tf fi.
set (A := Zo (powerset E)(fun x=> forall y, inc y x -> inc (f y) x)).
have AE:sub A (powerset E) by rewrite /A; apply Z_sub.
set (B:= complement E F).
set (C:= Zo A (fun x=> sub B x)).
have EC: inc E C by rewrite /C/A/B ! Z_rw; aw; ee; apply sub_complement.
set (D:= intersection C).
have p1: forall x, inc x C -> sub D x.
  move=> x xC; rewrite /D=> t tD; apply (intersection_forall tD xC).
have DA: inc D A.
  rewrite /A; apply Z_inc.
   by apply powerset_inc; apply intersection_sub => //.
   move=> y yD; apply intersection_inc; first by ex_tac.
   move=> t tC.
   move: (intersection_forall yD tC) => yt.
   by move: tC; rewrite Z_rw /A Z_rw; move=> [[_ tp] _]; apply tp.
have DC: inc D C.
   apply Z_inc =>//;rewrite /D=> t tD; apply intersection_inc; first by ex_tac.
   by move=> y; rewrite /C Z_rw; move=>[_]; apply.
have BD: sub B D by move: DC; rewrite /C Z_rw; intuition.
have cEB: (complement E B= F) by apply double_complement.
have Dst: (forall y : Set, inc y D -> inc (f y) D).
  by move: DA; rewrite /A Z_rw; intuition.
exists (BL (fun y => Yo (inc y D) (f y) y) E F).
aw;ee; apply bl_bijective.
    move=> y yE /=; Ytac1 yD; [apply tf => // | rewrite -cEB; srw; ee ].
  move=> u v uE vE; Ytac1 uD; Ytac1 vD => //; try (apply fi => //).
    by move=> h; rewrite -h in vD; elim vD; apply Dst.
  by move=> h; rewrite h in uD; elim uD; apply Dst.
move=> y yF; case (inc_or_not y D) => yD; last by exists y; Ytac0; ee.
have DE:sub D E by move: DA; rewrite /A Z_rw; aw; move => [ok _].
set (T:= complement D (singleton y)).
have BT: sub B T.
  move=> t tB; move: yF; rewrite /T -cEB; srw; aw; move=> [_ nyB].
  by split; [ apply BD | dneg ty; rewrite -ty].
have TA: (~ (inc T A)).
  move=> TA.
  have TC: (inc T C) by apply Z_inc.
  move: ((p1 _ TC) _ yD); rewrite /T; srw; aw; intuition.
have [x [xT nfT]]: exists x, inc x T & ~ (inc (f x) T).
  apply exists_proof; dneg aux; apply Z_inc.
    aw; apply sub_trans with D => //; apply sub_complement.
  move=> z zT; case (inc_or_not (f z) T) => //; move => nfzt; elim (aux z);ee.
move: xT; rewrite /T; srw; aw; move=> [xD nxy].
exists x; split; first by apply DE.
Ytac0;ex_middle fxy; elim nfT; rewrite /T; srw; aw; ee.
Qed.

Lemma equipotent_restriction1: forall f x,
  sub x (source f) -> injection f ->
  x \Eq (image_by_fun f x).
Proof.
move=> f x wsf bf.
exists (restriction1 f x); split.
apply restriction1_bijective =>//; move: bf=>[]//.
by rewrite /restriction1; aw.
Qed.

Lemma equipotent_range: forall f, injection f ->
  (source f) \Eq (range (graph f)).
Proof.
move=> f injf; rewrite -image_by_fun_source; last by fct_tac.
apply equipotent_restriction1 => //; fprops.
Qed.

Theorem CantorBernstein: forall X Y,
  (exists f, injection f & source f = X & target f = Y) ->
  (exists f, injection f & source f = Y & target f = X) ->
  (exists f, bijection f & source f = X & target f = Y).
Proof.
move=> X Y [f1 [if1 [sf1 tf1]]][f2 [if2 [sf2 tf2]]].
set Z := image_by_fun f2 Y.
have e1: Y \Eq Z by apply equipotent_restriction1 => //; rewrite sf2; fprops.
have e2: X \Eq Z.
  set g:= fun w => W (W w f1) f2.
  have ff2: is_function f2 by fct_tac.
  have ff1: is_function f1 by fct_tac.
  move: (f_range_graph ff2) => rg2.
  move: (image_by_fun_source ff2); rewrite sf2 -/Z => zv.
  apply Cantor_Bernstein1 with g.
     rewrite zv -tf2 //.
    rewrite -sf1 zv /g; move=> x xs.
    rewrite (range_inc_rw _ ff2); exists (W x f1); ee.
    rewrite sf2 -tf1; apply inc_W_target =>//.
  rewrite -sf1 /g; move=> x y xs ys sg.
  move: if1 => [_ prop]; apply prop => //.
  move: if2 => [_ prop2].
  apply prop2 => //;rewrite sf2 -tf1;apply inc_W_target =>//.
have : X \Eq Y by eqtrans Z; eqsym.
done.
Qed.

Definition transitive_set X:= forall x, inc x X -> sub x X.
Definition decent_set x := forall y, inc y x -> ~ (inc y y).
Definition asymmetric_set E :=
  forall x y, inc x E -> inc y E -> inc x y -> inc y x -> False.
Definition ordinal_oa E := graph_on (fun a b => inc a b \/ a = b) E.
Definition ordinal_o x := inclusion_suborder x.
Definition succ_o x := tack_on x x.

Lemma transitive_union: forall x, (forall y, inc y x -> transitive_set y)
  -> transitive_set (union x).
Proof.
move=> x alt a au t ta.
move: (union_exists au)=> [y [ay yx]].
move: (((alt _ yx) _ ay) _ ta) => ty; union_tac.
Qed.

Lemma decent_union: forall x, (forall y, inc y x -> decent_set y)
  -> decent_set (union x).
Proof.
move=> x alt a au aa.
move: (union_exists au)=> [y [ay yx]].
by elim ((alt _ yx) _ ay).
Qed.

Lemma transitive_intersection: forall x,
  (forall y, inc y x -> transitive_set y)
  -> nonempty x -> transitive_set (intersection x).
Proof.
move=> x alt nea a au t ta.
apply intersection_inc => //.
move=> y yx.
apply ((alt _ yx) _ (intersection_forall au yx)) =>//.
Qed.

Lemma decent_intersection: forall x,
  (forall y, inc y x -> decent_set y)
  -> nonempty x -> decent_set (intersection x).
Proof.
move=> x alt nea a au aa.
move: nea => [y yx].
by apply ((alt _ yx) _ (intersection_forall au yx)) .
Qed.

Lemma transitive_succ: forall y,
  transitive_set y -> transitive_set (succ_o y).
Proof.
rewrite /succ_o=>y ty z; aw; case => h.
  move =>t tz; move: ((ty _ h) _ tz); aw; intuition.
rewrite h; move=> u uy; fprops.
Qed.

Lemma decent_succ: forall y,
  decent_set y -> decent_set (succ_o y).
Proof.
rewrite /succ_o=>y ty z; aw; case => h.
  by apply ty.
move=> zz;have zy:inc z y by ue.
by elim (ty _ zy).
Qed.

Definition is_ordinal X:= forall Y, sub Y X -> transitive_set Y ->
  Y <> X -> inc Y X.

Lemma ordinal_succ: forall x,
  is_ordinal x -> is_ordinal (succ_o x).
Proof.
rewrite /succ_o; move=> x or y ytx tsy yntxx.
case (inc_or_not x y) => h.
  elim yntxx; apply extensionality=>//.
  move=> t; aw; move: (tsy _ h) => xy.
  by case=> tx; last (by rewrite tx); apply xy.
have syx: (sub y x).
   move=> t ty; move: (ytx _ ty); aw; case; first by intuition.
   move=> tx; elim h; ue.
case (equal_or_not y x)=> h'; first by rewrite h'; fprops.
by aw; left; apply or.
Qed.

Lemma ordinal_transitive_decent: forall x,
  is_ordinal x -> (transitive_set x & decent_set x).
Proof.
move=> x ox.
set y:=Zo (powerset x) (fun z=> transitive_set z & decent_set z).
set t := union y.
have : transitive_set t & decent_set t.
  split; first by apply transitive_union=> z; rewrite /y Z_rw; intuition.
  apply decent_union=> z; rewrite /y Z_rw; intuition.
case: (p_or_not_p (t = x)); first by move=> ->.
move=> ntx [p1 p2].
have sux: sub t x by apply sub_union; move =>z; rewrite /y Z_rw; aw; intuition.
move: (ox _ sux p1 ntx)=> ux.
have itu: (inc t (succ_o t)) by rewrite /succ_o;fprops.
elim ((decent_succ p2) _ itu).
apply union_inc with (succ_o t) =>//.
rewrite /y; apply Z_inc.
  by rewrite /succ_o; aw; move=> u; aw; case; [apply sux | move=> ->].
by split; [apply transitive_succ | apply decent_succ].
Qed.

Lemma ordinal_transitive: forall x, is_ordinal x -> transitive_set x.
Proof. by move => x ox; move: (ordinal_transitive_decent ox)=> [].
Qed.

Lemma ordinal_decent: forall x, is_ordinal x -> decent_set x.
Proof. by move => x ox; move: (ordinal_transitive_decent ox)=> [].
Qed.

Lemma ordinal_irreflexive: forall x, is_ordinal x -> ~ (inc x x).
Proof.
move=> x ox; move: (ordinal_decent ox) => dx.
by move=> xx; elim (dx _ xx).
Qed.

Lemma ordinal_sub: forall x y,
  is_ordinal x -> is_ordinal y -> sub x y ->
  x = y \/ inc x y.
Proof.
move=> x y ox oy xy; case (equal_or_not x y); first by intuition.
move=> nxy; right; apply oy => //.
apply: (ordinal_transitive ox).
Qed.

Lemma ordinal_sub2: forall x y, is_ordinal y ->
  inc x y -> strict_sub x y.
Proof.
move=> x y oy xy;move: (ordinal_transitive_decent oy)=> [ty dy].
split; first by apply ty.
move: (dy _ xy)=> xx xx'; rewrite -xx' in xy; contradiction.
Qed.

Lemma ordinal_sub3: forall x y, is_ordinal y ->
  inc x (succ_o y) -> sub x y.
Proof.
move=> x y yb; rewrite /succ_o; aw; case => h.
  apply (ordinal_transitive yb h).
rewrite h; fprops.
Qed.

Lemma ordinal_sub4: forall x y, is_ordinal x -> is_ordinal y ->
  sub x y = inc x (succ_o y).
Proof.
move=> x y xb yb; apply iff_eq; last by apply ordinal_sub3.
move=> h; rewrite /succ_o; aw; case (ordinal_sub xb yb h); intuition.
Qed.

Definition ordinal_set E := (forall i, inc i E -> is_ordinal i).

Lemma ordinal_intersection: forall x, nonempty x -> ordinal_set x ->
   inc (intersection x) x.
Proof.
move=> x nex alo.
case (inc_or_not (intersection x) x)=> // nux.
have iii: inc (intersection x) (intersection x).
  apply intersection_inc =>//.
  move => a ax; move: (alo _ ax) => oa.
  have su: (sub (intersection x) a).
    move=>t tix; apply (intersection_forall tix ax).
  case (equal_or_not (intersection x) a).
    move => h1; rewrite -h1 in ax; contradiction.
  apply oa => //.
  apply transitive_intersection =>//.
  by move=> y yx; move: (ordinal_transitive (alo _ yx)).
have ou: (decent_set (intersection x)).
  apply decent_intersection =>//.
  by move=> y yx; move: (ordinal_transitive_decent (alo _ yx)) => [_].
by elim (ou _ iii).
Qed.

Lemma ordinal_trichotomy : forall x y,
  is_ordinal x -> is_ordinal y ->
  (inc x y \/ inc y x \/ x = y).
Proof.
move=> x y ox oy.
move: (nonempty_doubleton x y) => ne.
have aux: (forall a, inc a (doubleton x y) -> is_ordinal a).
  move=> a; rewrite doubleton_rw; case; move=> ->//.
move: (ordinal_intersection ne aux).
rewrite -[intersection (doubleton x y)]/(intersection2 x y).
rewrite doubleton_rw -intersection2_sub intersection2C -intersection2_sub.
case => h.
  case (ordinal_sub ox oy h); intuition.
  case (ordinal_sub oy ox h); intuition.
Qed.

Lemma ordinal_pr: forall x, transitive_set x -> ordinal_set x ->
  is_ordinal x.
Proof.
move=> x tx alo y sys ty nyx.
case (emptyset_dichot (complement x y))=> cxy.
  by elim nyx; apply extensionality =>//; apply empty_complement.
move: cxy=>[z]; srw ; move=> [zx nzy]; move: (alo _ zx)=> oz.
have zy: (sub y z).
  move=> t ty'; move: (alo _ (sys _ ty'))=> ot.
  case (ordinal_trichotomy oz ot)=> zt.
    by elim nzy; apply (ty _ ty').
  by case zt=>// => zt'; elim nzy; ue.
case (equal_or_not y z); first by move=> ->.
move=> yz; apply (tx _ zx _ (oz _ zy ty yz)).
Qed.

Lemma elt_of_ordinal: forall x y, is_ordinal x -> inc y x ->
  is_ordinal y.
Proof.
move=> x y ox yx.
set (t:= union (Zo(powerset x) (fun y=> transitive_set y &
  forall a, inc a y -> is_ordinal a))).
have tp: forall z, inc z t -> is_ordinal z.
  move => z; rewrite /t; srw; move=>[v [zv]]; rewrite Z_rw.
  by move=> [_ [_ aux]]; apply aux.
apply tp.
have ot: is_ordinal t.
  apply ordinal_pr=> //.
  apply transitive_union; move=> t'; rewrite Z_rw; intuition.
suff: t=x by move=> ->.
case (ordinal_trichotomy ox ot).
  rewrite {1} /t; srw; move=> [v [xv]]; rewrite Z_rw; aw.
  move=> [aux _]; move: (aux _ xv)=> xx.
  by elim (ordinal_irreflexive ox).
case =>// tx.
move: (ordinal_transitive ox)=> trx.
move: (ordinal_succ ot)=> ort.
elim (ordinal_irreflexive ot).
apply union_inc with (tack_on t t); fprops.
apply Z_inc; first by aw; move=> z; aw; case; [ apply trx | move=> ->].
split; first by apply (ordinal_transitive ort).
by move=> u; aw; case; [ apply tp |move=> ->// ].
Qed.

Ltac ord_tac0 :=
 match goal with
  | h1: is_ordinal ?a, h2: inc ?b ?a |- is_ordinal ?b =>
    apply (elt_of_ordinal h1 h2)
  | h1: is_ordinal ?x, h2: inc ?y ?x, h3: inc ?z ?y |- inc ?z ?x =>
    apply (((ordinal_transitive h1) _ h2) _ h3)
end.

Lemma non_collectivizing_ordinal:
  ~(exists x, forall a, is_ordinal a -> inc a x).
Proof.
move=> [x xp]; set (y := Zo x is_ordinal).
have yp: forall a, inc a y = is_ordinal a.
  move=> a; rewrite /y Z_rw; apply iff_eq; [ intuition | move=> aB; ee].
have yB: is_ordinal y.
  apply ordinal_pr.
    move=> a ay b ba; rewrite yp in ay; rewrite yp; ord_tac0.
  by move=> b; rewrite yp.
by elim (ordinal_irreflexive yB); rewrite yp.
Qed.

Lemma ordinal_asymmetric: forall E, is_ordinal E -> asymmetric_set E.
Proof.
move=> E BE x y xE yE xy yx.
have h1: is_ordinal x by ord_tac0.
have: inc x x by ord_tac0.
by apply ordinal_irreflexive.
Qed.

Lemma ordinal_same_wo: forall x, is_ordinal x ->
  ordinal_oa x = ordinal_o x.
Proof.
move=> x ox.
rewrite /ordinal_oa/ordinal_o/inclusion_suborder/graph_on.
set_extens t; rewrite !Z_rw; aw; move=> [[pt [Px Qx]] aux]; ee.
  case aux; last by move=> -> ; fprops.
  by move=> ipq; move: (ordinal_sub2 (elt_of_ordinal ox Qx) ipq)=> [h _].
move: (ordinal_sub (elt_of_ordinal ox Px) (elt_of_ordinal ox Qx) aux).
intuition.
Qed.

Lemma ordinal_o_lt: forall a b c, is_ordinal c ->
   inc a c -> inc b c ->
   glt (ordinal_o c) a b = inc a b.
Proof.
move=> a b c oc ac bc; rewrite /glt/ordinal_o; aw.
move: (elt_of_ordinal oc bc) => ob.
apply iff_eq.
   move=> [[h1 [h2 h3]] h4].
  case (ordinal_sub (elt_of_ordinal oc ac) ob h3) => //.
move=> ab; move: (ordinal_sub2 ob ab)=> [ h1 h2]; ee.
Qed.

Definition least_ordinal (p: Set -> Prop) x:= intersection (Zo (succ_o x) p).

Lemma ordinal_worder1: forall x (p: Set -> Prop),
  is_ordinal x -> (p x) ->
  let y:= least_ordinal p x in
    (is_ordinal y & p y & forall z, is_ordinal z -> p z -> sub y z).
Proof.
move=> x p bx px.
set (t:= Zo (succ_o x) p).
have xt: inc x t by rewrite /t Z_rw /succ_o; aw; fprops.
have net: nonempty t by exists x.
have alo: (forall a, inc a t -> is_ordinal a).
  move=> a; rewrite /t Z_rw; move=> [ak _].
  move: (ordinal_succ bx) => aux; ord_tac0.
move:(ordinal_intersection net alo) => h.
simpl; ee.
  by move: h; rewrite {2}/t Z_rw; move =>[_].
have sxt: sub (intersection t) x by apply intersection_sub.
move=> z oz pz.
case: (ordinal_trichotomy bx oz) => ty.
  by apply sub_trans with x => //; apply (ordinal_transitive oz).
have zt: inc z t by rewrite /t Z_rw /succ_o; aw; ee.
by move=> w wi; apply (intersection_forall wi zt).
Qed.

Lemma ordinal_worder2: forall x, is_ordinal x ->
  worder (ordinal_o x).
Proof.
move=> E BE.
rewrite /ordinal_o.
split; fprops; rewrite substrate_subinclusion_order.
move=> x xE nex.
have p1: (forall a, inc a x -> is_ordinal a).
  move=> a ax; move: (xE _ ax) => aE; ord_tac0.
move: (ordinal_intersection nex p1) => ix.
exists (intersection x); red;aw; fprops; ee.
by move=> y yx; aw; ee; apply intersection_sub.
Qed.

Lemma ordinal_worder: forall x, is_ordinal x ->
  worder (ordinal_oa x).
Proof.
move=> E BE; rewrite ordinal_same_wo //; by apply ordinal_worder2.
Qed.

Lemma ordinal_segment1: forall E x, decent_set E -> transitive_set E->
  inc x E -> segment (ordinal_oa E) x = x.
Proof.
move => E x dE tE xE.
have ->: segment (ordinal_oa E) x = intersection2 x E.
  rewrite /segment/interval_uo /ordinal_oa.
  have p0:forall a , inc a E -> inc a a \/ a = a by move=> a aE; intuition.
  rewrite substrate_graph_on //.
  set_extens y; rewrite Z_rw /glt /gle graph_on_rw1; aw.
    intuition.
  move=> [yx yE]; ee; move=> xy; rewrite xy in yx; elim (dE _ xE yx).
by rewrite -intersection2_sub; apply tE.
Qed.

Lemma ordinal_segment: forall E x, is_ordinal E ->
  inc x E -> segment (ordinal_o E) x = x.
Proof.
move=> E x ox xE;rewrite -ordinal_same_wo //.
apply ordinal_segment1 => //.
  apply ordinal_decent => //.
apply ordinal_transitive => //.
Qed.

Lemma ordinal_pr1: forall E,
  is_ordinal E = (transitive_set E & worder (ordinal_oa E) & asymmetric_set E).
Proof.
move=> E; apply iff_eq.
  move=> h; ee.
  by apply ordinal_transitive.
  by apply ordinal_worder.
  by apply ordinal_asymmetric.
move=> [tE [woE aE]] X XE tX nXE.
have de: decent_set E.
  move=> u uE uu; elim (aE _ _ uE uE uu uu).
have p0:forall b, inc b E -> inc b b \/ b = b by move=> b bE; intuition.
have sg: (substrate (ordinal_oa E)) = E.
  by rewrite /ordinal_oa substrate_graph_on //.
have si: is_segment (ordinal_oa E) X.
  rewrite /is_segment/interval_uo /ordinal_oa sg; split => //.
  move=> x y; rewrite /gle graph_on_rw1; aw; move=> xX [yE [_ h]].
  case h; [ apply (tX _ xX) | by move => -> ].
case (well_ordered_segment woE si).
  rewrite sg; move=> eXE; contradiction.
rewrite sg; move=> [x [xs Xs]]; rewrite Xs ordinal_segment1 //.
Qed.

Lemma ordinal_isomorphism_unique: forall x y f,
  is_ordinal x -> is_ordinal y ->
  order_isomorphism f (ordinal_o x)(ordinal_o y) ->
  (x = y & f = identity x).
Proof.
move=> x y f ox oy oif.
move: (oif) => [_ [_ [[[ff injf] surf] [srcf [trgf pf]]]]].
move: srcf trgf; rewrite /ordinal_o !substrate_subinclusion_order => srcf trgf.
have Wt: forall a, inc a x -> inc (W a f) y.
  by move=> a; rewrite srcf trgf => asf; apply inc_W_target.
have prf2:forall a b, inc a x -> inc b x -> inc a b = inc (W a f) (W b f).
  move=> a b ax bx.
  rewrite !srcf in ax bx; move: (order_isomorphism_pr1 oif ax bx).
  rewrite -! ordinal_same_wo //.
  rewrite /glt/gle /ordinal_oa ! graph_on_rw1 => h.
  rewrite -!srcf in ax bx; apply iff_eq => aux.
    have: ((inc a x & inc b x & inc a b \/ a = b) & a <> b).
      by ee; move=> ab; rewrite ab in aux; elim (ordinal_decent ox bx).
    rewrite h; move=> [[_ [_ h1]] ne]; by case h1.
  have: ((inc a x & inc b x & inc a b \/ a = b) & a <> b).
    rewrite h; ee; move=> ab; rewrite ab in aux.
    by elim (ordinal_decent oy (Wt _ bx)).
  move=> [[_ [_ h1]] ne]; by case h1.
have surjf: forall b, inc b y -> exists a, inc a x & W a f =b.
  rewrite trgf srcf; move=> b bt.
  move: (surjective_pr2 surf bt)=> [a [asf Wa]]; exists a;intuition.
set (A:=Zo x(fun z => W z f <> z)).
case (emptyset_dichot A)=> Ae.
  have fi: forall a, inc a x -> W a f = a.
    by move=> a ax; ex_middle em; empty_tac1 a; rewrite /A; apply Z_inc.
  have xy: x = y.
    set_extens t => tx.
       rewrite -(fi _ tx) trgf; apply inc_W_target =>//; ue.
    by move: (surjf _ tx)=> [z [zx]]; move => <-;rewrite (fi _ zx).
  split => //.
  apply function_exten;aw; ee.
    by rewrite xy.
  by move=> a; rewrite -srcf;move=> ax; rewrite identity_W //; apply fi.
have p0: (forall a, inc a A -> is_ordinal a).
  by move=> a; rewrite /A Z_rw; move=> [ax _]; ord_tac0.
move: (ordinal_intersection Ae p0) => iA.
set B := intersection A.
move: iA;rewrite -/B; rewrite /A Z_rw; move=> [Bx WB].
have sBx: sub B x by apply (ordinal_transitive ox).
move: (elt_of_ordinal ox Bx) => orB.
have p1: forall a, inc a B -> W a f = a.
  move=> a aB; ex_middle aux.
  have aA: inc a A.
    rewrite /A; apply Z_inc => //; apply (sBx _ aB).
  have Ba: sub B a by rewrite /B; apply intersection_sub.
  elim ((ordinal_decent orB) _ aB); apply (Ba _ aB).
have By: sub B y.
   move=> a aB; rewrite -(p1 _ aB) //; apply Wt; apply (sBx _ aB).
move: (ordinal_transitive orB) => tB.
have sB: sub B (W B f) by move => a aB; rewrite -(p1 _ aB) -prf2 //;apply sBx.
have sB1: inc B (W B f).
  case (ordinal_sub orB (elt_of_ordinal oy (Wt _ Bx)) sB)=>//.
  move=> h; symmetry in h;contradiction.
have nBy: B <> y.
  dneg eBy; move: (Wt _ Bx); rewrite -eBy => h; rewrite -srcf in injf.
  move: (p1 _ h) => h1; apply: (injf _ _ (sBx _ h) Bx h1).
move: (surjf _ (oy _ By tB nBy)) => [a [ax wa]].
case (ordinal_trichotomy orB (elt_of_ordinal ox ax)).
  rewrite (prf2 _ _ Bx ax); rewrite wa => h.
  elim (ordinal_decent orB h (sB _ h)).
case; last by move=> h; rewrite -h in wa; contradiction.
move=> h; rewrite (p1 _ h) in wa; rewrite wa in h.
elim (ordinal_irreflexive orB h).
Qed.

Lemma ordinal_isomorphism_exists: forall r, worder r ->
  let f := transfinite_defined r target in
  is_ordinal (target f) &
  order_isomorphism f r (ordinal_o (target f)).
Proof.
move=> r wor f.
move: (wor)=> [or worp].
move: (transfinite_defined_pr target wor) => [suf [sf vf]].
rewrite -/f in suf sf vf.
set E:= substrate r.
have fa: is_function f by fct_tac.
have vf1: forall a b, inc a E ->
  inc b (W a f) = (exists u, glt r u a & W u f = b).
  move=> a b aE; rewrite (vf _ aE) /restriction_to_segment /restriction1; aw.
    apply iff_eq; move=> [u h]; exists u; first by rewrite -segment_rw//.
    rewrite segment_rw //.
  rewrite sf; apply sub_segment => //.
have incf3: forall a b, inc a (source f) -> inc b (source f) ->
     sub (W a f) (W b f) -> gle r a b.
  rewrite sf => a b aE bE sab.
  case (total_order_pr2 (worder_total wor) bE aE) => // ltab.
  set (Bad:= Zo E (fun a => inc (W a f) (W a f))).
  case (emptyset_dichot Bad)=> h.
     empty_tac1 b; rewrite /Bad; apply Z_inc =>//.
     apply sab; rewrite (vf1 _ _ aE); exists b; split=>//.
  have BE: (sub Bad E) by rewrite /Bad; apply Z_sub.
  move: (worp _ BE h) => [y[]]; aw; rewrite /Bad Z_rw; move=> [yE iWWy] yp.
  move: (iWWy); rewrite (vf1 _ _ yE); move=> [u [us Wu]].
  have badu: inc u Bad by apply Z_inc=>//; [rewrite /E;order_tac | ue ].
  move: (iorder_gle1 (yp _ badu)) => yu; order_tac.
have injf: injection f.
  split=>//; move=> x y xsf ysf Wxy.
  have p1: sub (W x f) (W y f) by rewrite Wxy; fprops.
  have p2: sub (W y f) (W x f) by rewrite Wxy; fprops.
  move: (incf3 _ _ xsf ysf p1) (incf3 _ _ ysf xsf p2) => p3 p4; order_tac.
have incf: (forall a b, gle r a b -> sub (W a f) (W b f)).
  move=> a b ab t.
  have aE: (inc a E) by rewrite /E; order_tac.
  have bE: (inc b E) by rewrite /E; order_tac.
  rewrite (vf1 _ _ bE)(vf1 _ _ aE); move=> [u [us h]]; exists u; ee; order_tac.
have oi: (order_isomorphism f r (ordinal_o (target f))).
  red; ee; first (by split =>//); aw.
  move=> x y xsf ysf; aw; apply iff_eq.
    move=> xy;ee; try apply inc_W_target=>//.
  move=> [Wxt [Wyt xy]]; apply (incf3 _ _ xsf ysf xy).
split=>//; apply ordinal_pr.
  move=> x xt y.
  move: (surjective_pr2 suf xt)=> [z [zs]] <-.
  rewrite sf in zs; rewrite (vf1 _ _ zs).
  move=> [u [us Jg]]; rewrite -Jg; apply inc_W_target => //.
  rewrite sf; order_tac.
move=> y ytf; move: (surjective_pr2 suf ytf)=> [z [zs]] <-.
set (Bad:= Zo E (fun z => (~ (is_ordinal (W z f))))).
case (emptyset_dichot Bad)=> h.
  by ex_middle h'; empty_tac1 z; rewrite /Bad; apply Z_inc =>//; rewrite /E -sf.
have sBE:sub Bad E by rewrite /Bad; apply Z_sub.
move: (worp _ sBE h) => [x []]; aw; rewrite /Bad Z_rw; move=> [xE ioWx] xp.
elim ioWx; apply ordinal_pr.
  move=> b; rewrite (vf1 _ _ xE).
  move=> [u [[ua _] Wu]] t tb; move: (incf _ _ ua); apply; ue.
move => a; rewrite (vf1 _ _ xE); move=> [u [usr Wu]]; rewrite -Wu.
ex_middle h'.
have ub:inc u Bad by rewrite /Bad ; apply Z_inc=>//; rewrite /E;order_tac.
move: (iorder_gle1 (xp _ ub)) => yu; order_tac.
Qed.

Definition ordinal r := target (transfinite_defined r target).

Lemma ordinal_p1: forall r, worder r -> is_ordinal (ordinal r).
Proof.
by move=> r wor; move:(ordinal_isomorphism_exists wor) => [h _].
Qed.

Lemma ordinal_p2: forall r, worder r ->
  order_isomorphic r (ordinal_o (ordinal r)).
Proof.
move=> r wor; move:(ordinal_isomorphism_exists wor) => [_ h].
by exists (transfinite_defined r target).
Qed.

Lemma ordinal_p3: forall E, is_ordinal E->
  ordinal (ordinal_o E) = E.
Proof.
move=> E BE; move: (ordinal_worder2 BE)=> woi.
symmetry.
set F:= (ordinal_o E).
move: (ordinal_isomorphism_exists woi) => [_ ].
set f := transfinite_defined _ _.
have ->: target f = ordinal F by rewrite /f /ordinal.
move=> h.
by move: (ordinal_isomorphism_unique BE (ordinal_p1 woi) h) => [res _].
Qed.

Lemma ordinal_p4: forall x y,
  is_ordinal x -> is_ordinal y ->
  (ordinal_o x) \Is (ordinal_o y) -> x = y.
Proof.
move=> x y ox oy [f fi]; move: (ordinal_isomorphism_unique ox oy fi).
intuition.
Qed.

Lemma ordinal_p5: forall x y z,
  is_ordinal x -> is_ordinal y ->
  (ordinal_o x) \Is z -> (ordinal_o y) \Is z ->
  x = y.
Proof.
move=> x y z ox oy oi1 oi2.
move: (orderIT oi1 (orderIS oi2)) => oi3.
by apply ordinal_p4.
Qed.

Lemma ordinal_p7: forall E, is_ordinal E -> substrate (ordinal_o E) = E.
Proof. by move => E EB; rewrite /ordinal_o substrate_subinclusion_order. Qed.

Definition order_le r r' :=
  order r & order r' &
  exists f, exists x,
    sub x (substrate r') & order_isomorphism f r (induced_order r' x).
Definition ordinal_le r r' :=
  is_ordinal r & is_ordinal r' & order_le (ordinal_o r)(ordinal_o r').
Definition ordinal_lt r r' := ordinal_le r r' & r <> r'.

Notation "x <=o y" := (ordinal_le x y) (at level 50).
Notation "x <o y" := (ordinal_lt x y) (at level 50).

Lemma order_le_compatible: forall r r' r1 r1',
  r \Is r1 -> r' \Is r1' ->
  (order_le r r' = order_le r1 r1').
Proof.
suff: forall r1 r2 r3 r4, r1 \Is r3 -> r2 \Is r4 ->
  order_le r1 r2 -> order_le r3 r4.
  by move=> aux r1 r2 r3 r4 p1 p2; apply iff_eq; apply aux=>//; apply orderIS.
move => r1 r2 r3 r4 o13.
move: (orderIS o13)=> [f [o3 [_ [[injf srf] [sf [tf oif]]]]]].
move=> [g [_ [o4 [[ig srg] [sg [tg oig]]]]]].
move=> [o1 [o2 [h [X [sX [_ [_ [[ih srh] [sh [th oih]]]]]]]]]].
red; ee.
set Y:= image_by_fun g X.
have sY: sub Y (substrate r4).
  by rewrite /Y tg; apply sub_image_target1; fct_tac.
have fg: is_function g by fct_tac.
have ff: is_function f by fct_tac.
have fh: is_function h by fct_tac.
have sX': sub X (source g) by ue.
have Yp1: forall x, inc x X -> inc (W x g) Y.
  by move=> x; rewrite /Y; aw; move=> xX; ex_tac.
have Yp2: forall y, inc y Y -> exists x, inc x X & W x g = y.
  by move=> y; rewrite /Y; aw.
awi th => //.
set k:= fun x => W (W (W x f) h) g.
have ta1: forall x, inc x (substrate r3) -> inc (k x) Y.
  rewrite sf /k; move=> t ts; apply Yp1.
  move: (inc_W_target ff ts); rewrite -tf sh => Wt.
  rewrite th; apply inc_W_target=> //;fct_tac.
exists (BL k (substrate r3) Y); exists Y; ee.
red; rewrite bl_source; ee.
    apply bl_bijective => //.
      rewrite sf; move=> u v us vs eq.
      move: (inc_W_target ff us) (inc_W_target ff vs) => Wt1 Wt2.
      rewrite -tf sh in Wt1 Wt2.
      move: (inc_W_target fh Wt1)(inc_W_target fh Wt2).
      rewrite -th; aw => Wt3 Wt4.
      move: ig=> [_ bi];rewrite -sg in bi.
      move: (bi _ _ (sX _ Wt3) (sX _ Wt4) eq) => eq1.
      move: ih=> [_ bi1];move: (bi1 _ _ Wt1 Wt2 eq1) => eq2.
      move: injf=> [_ bi2]; apply bi2 => //.
    move=> t tY; move: (Yp2 _ tY) => [x [xX]] <-.
    rewrite th in xX; move: (surjective_pr2 srh xX)=> [v [vsf]] <-.
    rewrite -sh tf in vsf.
    move: (surjective_pr2 srf vsf)=> [w [wsc]] <-.
    rewrite sf; ex_tac.
  aw.
move=> u v us vs; aw; try apply ta1 =>//.
rewrite sf in us vs; rewrite oif //.
move: (inc_W_target ff us) (inc_W_target ff vs) => Wt1 Wt2.
rewrite -tf sh in Wt1 Wt2;rewrite oih //.
move: (inc_W_target fh Wt1)(inc_W_target fh Wt2).
rewrite -th=> Wt3 Wt4; aw.
by rewrite oig //; apply sX'.
Qed.

Lemma order_le_compatible1: forall r r',
  worder r -> worder r' ->
  order_le r r' = (ordinal r) <=o (ordinal r').
Proof.
move=> r r' wo1 wo2.
move: (ordinal_p2 wo1)(ordinal_p2 wo2) => oi1 oi2.
move: (ordinal_p1 wo1)(ordinal_p1 wo2) => o1 o2.
rewrite (order_le_compatible oi1 oi2); rewrite /ordinal_le.
apply iff_eq; intuition.
Qed.

Lemma ordinal_le_pr: forall x x',
   x <=o x' = (
    is_ordinal x & is_ordinal x' &
     exists f, exists S,
      is_segment (ordinal_o x') S &
      order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') S)).
Proof.
move=> r r';apply iff_eq.
  move=> [or [or' [otr [otr' [f [x [sx iso]]]]]]]; ee.
  move:(isomorphic_subset_segment (ordinal_worder2 or') sx) => [w [g [sw isg]]].
  exists (g \co f); exists w; ee.
  apply (compose_order_isomorphism iso isg).
move=> [or [or' [f [x [[sx sxp] oi]]]]]; red; ee.
red; ee; exists f; exists x; ee.
Qed.

Lemma ordinal_le_pr1: forall x x',
   ordinal_le x x' = (
    is_ordinal x & is_ordinal x' &
     exists f, is_segment (ordinal_o x') (range (graph f)) &
         order_morphism f (ordinal_o x)(ordinal_o x')).
Proof.
move=> r r'; symmetry;apply iff_eq.
  move=> [or [or'[f [_ mf]]]]; red; ee.
  red; ee; try apply ordinal_pr10 =>//; apply order_le_alt.
      by move: (ordinal_worder2 or) => [ok _].
    by move: (ordinal_worder2 or') => [ok _].
  by exists f.
rewrite ordinal_le_pr; move => [or [or' [f [x [sx isof]]]]]; ee.
move: (ordinal_worder2 or) => [ora _].
move: (ordinal_worder2 or') => [orb _].
have sxs: sub x (substrate (ordinal_o r')) by apply sub_segment1.
move: (order_le_alt2 ora orb sxs isof).
set g := BL _ _ _.
move => [om xp]; exists g; rewrite xp; ee.
Qed.

Lemma ordinal_le_pr2: forall x y, is_ordinal x -> is_ordinal y -> sub x y ->
   induced_order (ordinal_o y) x = (ordinal_o x).
Proof.
move=> x y ox oy xy.
rewrite /ordinal_o/induced_order/ordinal_o/graph_on/coarse.
set_extens t; aw; rewrite ! Z_rw; aw; intuition.
Qed.

Lemma ordinal_le_pr3: forall x y, is_ordinal y -> inc x y ->
   induced_order (ordinal_o y) x = (ordinal_o x).
Proof.
move=> x y oy xy.
move: (elt_of_ordinal oy xy) => ox.
move: (ordinal_sub2 oy xy) => [sxy _].
apply (ordinal_le_pr2 ox oy sxy).
Qed.

Lemma ordinal_le_pr0: forall x y,
  x <=o y = (is_ordinal x & is_ordinal y & sub x y).
Proof.
move=> x y; apply iff_eq; last first.
  rewrite /ordinal_le; move=> [ox [oy sxy]]; ee.
  move: (ordinal_worder2 ox) => wox.
  move: (wox) => [orx _].
  red; rewrite ordinal_p7; ee.
  exists (identity x); exists x; ee.
  rewrite - {1} (ordinal_p7 ox) (ordinal_le_pr2 ox oy sxy).
  by apply identity_isomorphism.
rewrite ordinal_le_pr.
move => [ox [oy [f [S [sS oi]]]]]; ee.
move: (ordinal_worder2 oy) => woy.
have [p1 [p2 p3]]:
     (sub S y & is_ordinal S & (induced_order (ordinal_o y) S) = ordinal_o S).
  case (well_ordered_segment woy sS).
    move=> Ss; rewrite {3} Ss; move: Ss; rewrite {1} ordinal_p7 =>//.
    move => ->; ee; rewrite induced_order_substrate //.
    by move: woy => [ok _].
  move=> [u]; rewrite ordinal_p7 =>//.
  move => [uy].
  rewrite ordinal_segment //.
  move: (ordinal_transitive oy uy) => suy.
  move=> ->; ee; first by ord_tac0.
  rewrite /ordinal_o/induced_order/ordinal_o/graph_on/coarse.
  set_extens t; aw; rewrite ! Z_rw; aw; intuition.
rewrite p3 in oi.
move: (ordinal_isomorphism_unique ox p2 oi).
by move=>[h _]; rewrite h.
Qed.

Lemma ordinal_lt_pr0: forall x y,
  x <o y = (is_ordinal x & is_ordinal y & inc x y).
Proof.
move=> x y;rewrite /ordinal_lt! ordinal_le_pr0.
apply iff_eq.
  move=> [[ox [oy sxy]] nxy]; ee; case (ordinal_sub ox oy sxy); intuition.
move=> [ox [oy xy]]; move: (ordinal_sub2 oy xy); rewrite /strict_sub.
intuition.
Qed.

Theorem wordering_ordinal_le: worder_r ordinal_le.
Proof.
split.
  split.
    move=> x y z; rewrite ! ordinal_le_pr0; move=> [Kx [Ky xy]][_ [Kz yz]].
    ee; by apply sub_trans with y.
  split.
    move=> x y;rewrite ! ordinal_le_pr0; move=> [Kx [Ky xy]][_ [_ yx]].
    by apply extensionality.
  move=> x y; rewrite ! ordinal_le_pr0; ee.
move=> x ale.
have alo: forall a, inc a x -> is_ordinal a.
  by move=> a ax; move: (ale _ ax); rewrite /ordinal_le; move => [h _].
move=> nex.
set y := (intersection x).
suff yx:inc y x.
  exists y.
  red; rewrite (substrate_graph_on) =>//; split=>//.
  move=> a ax;rewrite /gle graph_on_rw1; ee; rewrite ! ordinal_le_pr0 ; ee.
  move: (alo _ ax) (alo _ yx) => Ka Ky.
  by apply intersection_sub.
by apply ordinal_intersection.
Qed.

Lemma ordinal_le_order_r: order_r ordinal_le.
Proof.
by move: wordering_ordinal_le => [h1 _].
Qed.

Lemma ordinal_le_reflexive: forall x, is_ordinal x ->
   x <=o x.
Proof. move=> x or; rewrite ordinal_le_pr0; fprops. Qed.

Lemma ordinal_le_transitive: forall x y z,
  x <=o y -> y <=o z -> x <=o z.
Proof. move: ordinal_le_order_r => [p1 [p2 _]]; apply p1. Qed.

Lemma ordinal_le_antisymmetric: forall x y ,
  x <=o y -> y <=o x -> x = y.
Proof. move: ordinal_le_order_r => [p1 [p2 _]]; apply p2. Qed.

Lemma ordinal_le_antisymmetry1: forall a b,
  a <=o b -> b <o a -> False.
Proof.
by move=> a b ole [olt one]; elim one; apply ordinal_le_antisymmetric.
Qed.

Lemma ordinal_lt_le_trans: forall a b c,
  a <o b -> b <=o c -> a <o c.
Proof.
move=> a b c [ab nab] bc; split.
  apply (ordinal_le_transitive ab bc).
by dneg ac; rewrite -ac in bc; apply ordinal_le_antisymmetric.
Qed.

Lemma ordinal_le_lt_trans: forall a b c, a <=o b -> b <o c -> a <o c.
Proof.
move=> a b c ab [bc nbc]; split.
  apply (ordinal_le_transitive ab bc).
by dneg ca; rewrite ca in ab; apply ordinal_le_antisymmetric.
Qed.

Lemma ordinal_le_total_order1: forall a b,
  is_ordinal a -> is_ordinal b ->
  a <=o b \/ b <oa.
Proof.
move=> a b oa ob; rewrite ordinal_le_pr0 ordinal_lt_pr0.
case (ordinal_trichotomy oa ob).
 move => h; move: (ordinal_sub2 ob h) => [pa pb]; left; ee.
case; [ right | move=> ->; left]; ee.
Qed.

Lemma ordinal_le_total_order: forall a b,
  is_ordinal a -> is_ordinal b -> a <=o b \/ b <=o a.
Proof.
move=> a b oa ob.
case (ordinal_le_total_order1 oa ob); rewrite /ordinal_lt;intuition.
Qed.

Lemma ordinal_le_total_order2: forall a b,
  is_ordinal a -> is_ordinal b -> (sub a b \/ inc b a).
Proof.
move=> a b oa ob; case (ordinal_le_total_order1 oa ob);
  rewrite ?ordinal_le_pr0 ?ordinal_lt_pr0; intuition.
Qed.

Ltac ord_tac :=
  match goal with
    | h: ordinal_le _ ?x |- is_ordinal ?x
      => move: h => [_ [h _]]; exact h
    | h: ordinal_le ?x _ |- is_ordinal ?x
      => move: h => [h _]; exact h
    | h: ordinal_lt _ ?x |- is_ordinal ?x
      => move: h => [[_ [h _]] _]; exact h
    | h: ordinal_lt ?x _ |- is_ordinal ?x
      => move: h => [[h _] _]; exact h
    | h1: ordinal_le ?x ?y, h2: ordinal_le ?y ?x |- ?x = ?y
      => apply (ordinal_le_antisymmetric h1 h2)
    | h1: ordinal_le ?x ?y, h2: ordinal_le ?y ?z |- ordinal_le ?x ?z
      => apply (ordinal_le_transitive h1 h2)
    | h1: ordinal_lt ?x ?y, h2: ordinal_le ?y ?z |- ordinal_lt ?x ?z
      => apply (ordinal_lt_le_trans h1 h2)
    | h1: ordinal_le ?x ?y, h2: ordinal_lt ?y ?z |- ordinal_lt ?x ?z
      => apply (ordinal_le_lt_trans h1 h2)
    | h1: ordinal_le ?x ?y, h2: ordinal_lt ?y ?x |- _
      => elim (ordinal_le_antisymmetry1 h1 h2)
    | h1: is_ordinal ?x, h2: inc ?y ?x |- is_ordinal ?y
      => apply (elt_of_ordinal h1 h2)
    | h1: is_ordinal ?x |- ordinal_le ?x ?x
      => apply (ordinal_le_reflexive h1)
    | h1: ordinal_lt ?x ?y |- ordinal_le ?x ?y
      => by move: h1 => []
end.

Lemma ordinal_lt_pr1: forall x x',
   x <o x' = (
    is_ordinal x & is_ordinal x' &
     exists f, exists y,
        inc y x' &
        (range (graph f)) = segment (ordinal_o x') y
        & order_morphism f (ordinal_o x) (ordinal_o x')).
Proof.
move=> r r'; rewrite /ordinal_lt ordinal_le_pr1;apply iff_eq.
  move=> [[or [or' [f [srf om]]]] nrr'].
  case (well_ordered_segment (ordinal_worder2 or') srf).
  move=> v; elim nrr'; apply ordinal_p4 => //.
  move: om => [o1 [o2 [injf [sf [tf mf]]]]].
  exists f; red;ee; red; ee; apply surjective_pr4; [fct_tac |rewrite -tf v //].
  move=> [x [xsr rgf]].
  split => //; split => //; exists f; exists x; ee.
  by rewrite - (ordinal_p7 or').
move=> [or [or' [f [x [xsr [rgf om]]]]]].
move: (ordinal_worder2 or') => wodr.
move: (wodr)=> [odr _].
have p1: is_segment (ordinal_o r') (range (graph f)).
  by rewrite rgf;apply segment_is_segment =>//; rewrite ordinal_p7 //.
ee; first by exists f; ee.
move=> rr'; rewrite rr' in om.
move: (unique_isomorphism_onto_segment wodr p1 om) => idf.
have xrg: inc x (range (graph f)).
  move: om => [_ [_ [ [ff _] [sf _]]]].
  rewrite idf in ff.
  rewrite idf range_inc_rw //; aw; ex_tac; rewrite identity_W //.
rewrite rgf in xrg.
apply (not_in_segment xrg).
Qed.

Lemma ordinal_lt_pr2: forall a b,
  worder b -> a <o (ordinal b) ->
     exists f, exists x,
        inc x (substrate b) &
        (range (graph f)) = segment b x & order_morphism f (ordinal_o a) b.
Proof.
move=> a b ob ltab; move: (ltab) =>[[oa _] _]; move: ltab.
rewrite ordinal_lt_pr1; move=> [_ [op [f [x [xsp [rgx om]]]]]].
have [g oig]: order_isomorphic (ordinal_o (ordinal b)) b.
  by apply orderIS; apply (ordinal_p2 ob).
move: om (oig) => [o1 [o2 [fi [sf [tf pf]]]]][_ [o4 [[gi gs] [sg [tg pg]]]]].
have ff: is_function f by fct_tac.
have cfg: composable g f by red; ee; try fct_tac; ue.
rewrite ! ordinal_p7 // in tf sf sg.
have p0: injection (g \co f) by apply compose_injective => //.
have p2: is_function (g \co f) by fct_tac.
have p3: order_morphism (g \co f) (ordinal_o a) b.
  red; ee; aw; move=> u v asf bsf.
  rewrite ! compose_W // pf // pg// -sg tf; apply inc_W_target => //.
set y:= (W x g).
have p1: inc y (substrate b).
    by rewrite tg; apply inc_W_target; try fct_tac; ue.
exists (g \co f); exists y; ee.
set_extens u; rewrite range_inc_rw //; aw.
  move=> [v [vsf uvW]].
  have: inc (W v f) (segment (ordinal_o (ordinal b)) x).
     rewrite -rgx range_inc_rw //;ex_tac.
  rewrite ! segment_rw uvW /y compose_W //.
  by apply (order_isomorphism_pr2 oig).
rewrite segment_rw; move=> buy.
have utg: inc u (target g) by rewrite -tg; order_tac.
move: (surjective_pr2 gs utg) buy => [v [vsg Wvg]].
rewrite sg in xsp.
rewrite /y -Wvg -(order_isomorphism_pr1 oig vsg xsp) -segment_rw -rgx.
rewrite range_inc_rw //; move=> [w [wsf Ww]]; ex_tac; rewrite Ww compose_W //.
Qed.

Notation "\osup" := union (only parsing).
Notation "\csup" := union (only parsing).
Notation "\opred" := union (only parsing).

Lemma ord_sup_pr1: forall E, ordinal_set E ->
  is_ordinal (\osup E).
Proof.
move=> x alo; apply ordinal_pr.
  apply transitive_union =>//.
  by move=> y yx; apply ordinal_transitive; apply alo.
move=> y; srw; move=> [a [ya ax]].
apply (elt_of_ordinal (alo _ ax) ya).
Qed.

Definition ord_sup_pr E x:=
   is_ordinal x &
   forall y, x <=o y =
    (is_ordinal y & forall i, inc i E -> i <=o y).

Lemma ord_sup_unique: forall E x y,
  ord_sup_pr E x -> ord_sup_pr E y -> x = y.
Proof.
move=> E.
have p1: forall x, ord_sup_pr E x -> forall i, inc i E -> i <=o x.
  rewrite /ord_sup_pr; move=> x [ox Ex].
  have aux: x <=o x by ord_tac.
  by rewrite (Ex x) in aux; move: aux=> [_].
have p2: forall x y, ord_sup_pr E x -> is_ordinal y ->
  (forall i, inc i E -> i <=o y) -> x <=o y.
  rewrite /ord_sup_pr; move=> x y [ox opf] oy h; rewrite opf; ee.
move=> x y fx fy.
have ox: is_ordinal x by move: fx => [ox _ ].
have oy: is_ordinal y by move: fy => [oy _ ].
move: (p2 _ _ fy ox (p1 _ fx)) (p2 _ _ fx oy (p1 _ fy))=> h1 h2.
ord_tac.
Qed.

Lemma ord_sup_pr2: forall E, ordinal_set E ->
  ord_sup_pr E (\osup E).
Proof.
move => E alo.
move: (ord_sup_pr1 alo) => pB.
red;ee; move => y; apply iff_eq.
  move=> h; have oy: is_ordinal y by ord_tac.
  ee; move=> i iE.
  have iu: i <=o (union E).
    by rewrite ordinal_le_pr0; ee; apply union_sub.
  ord_tac.
move=> [oy aly].
rewrite ordinal_le_pr0;ee.
move=> i; srw. move=> [z [iz ze]].
by move: (aly _ ze); rewrite ordinal_le_pr0; move=> [_ [_]]; apply.
Qed.

Lemma ord_sup_pr3: forall E, ordinal_set E ->
  forall i, inc i E -> i <=o (\osup E).
Proof.
move=> E Ep; move: (ord_sup_pr2 Ep).
rewrite /ord_sup_pr; move=> [ox fx].
have aux: (union E) <=o (union E) by ord_tac.
by rewrite (fx (union E) ) in aux; move: aux=> [_].
Qed.

Lemma ord_sup_pr4: forall E y, ordinal_set E ->
  is_ordinal y -> (forall i, inc i E -> i <=o y) ->
  (\osup E) <=o y.
Proof.
move=> E y Ep oy h; move: (ord_sup_pr2 Ep).
rewrite /ord_sup_pr; move=> [ox opf]; rewrite opf; ee.
Qed.

Lemma ordinal_least: forall x, is_ordinal x -> emptyset <=o x.
Proof.
move=> x xB; rewrite ordinal_le_pr0; ee.
 move=> y yx ty ney; elim ney.
 apply extensionality=>//; apply emptyset_sub_any.
apply emptyset_sub_any.
Qed.

Lemma ordinal_succ_pr: forall x, is_ordinal x ->
  let z := succ_o x in
  x <o z & (forall w, x <o w -> z <=o w).
Proof.
move=> x Bx y; move: (ordinal_succ Bx)=> yB.
split; first by rewrite ordinal_lt_pr0; ee; rewrite /y /succ_o; fprops.
move=> w; rewrite ordinal_lt_pr0 ordinal_le_pr0; move=> [_ [ow xw]]; ee.
move=> t ; rewrite /y /succ_o; aw; case; last by move=> ->.
by apply (ordinal_transitive ow).
Qed.

Lemma limit_ordinal_pr0: forall x, is_ordinal x ->
  let p := exists y, x = succ_o y in
  let q := x = \opred x in
  (p \/ q) & (p -> q -> False).
Proof.
move=> x xB p q; unfold succ_o in p.
case (p_or_not_p q) => h.
  split; first (by intuition); move=> [y yt] _.
  have yx: inc y x by rewrite yt; fprops.
  have yB: is_ordinal y by ord_tac0.
  move: yx; rewrite h union_rw; move => [a [ya]]; rewrite yt; aw.
  case => aux.
    move: (elt_of_ordinal yB aux)=> aB.
    move: ((ordinal_transitive aB ya) _ aux).
    apply (ordinal_irreflexive aB).
  by rewrite aux in ya; apply (ordinal_irreflexive yB).
split; last (by intuition); left.
have p1: sub (union x) x.
  move=> t; rewrite union_rw; move=> [y [ty yx]]; ord_tac0.
case (p_or_not_p (sub x (union x))).
  by move=> p2; elim h; apply extensionality.
move=> p2.
have [y [yx yp]]: exists y, inc y x & (~ inc y (union x)).
  apply exists_proof; move=> ne; elim p2; move=> t tx.
  ex_middle tu; elim (ne t); intuition.
have p3: sub (tack_on y y) x.
  move =>t; aw;case; [ move=> ty;ord_tac0 | by move=> ->].
exists y; apply extensionality =>//.
move=> t tx; aw.
case (ordinal_trichotomy (elt_of_ordinal xB yx)(elt_of_ordinal xB tx)).
  move=> yt; elim yp; apply union_inc with t =>//.
intuition.
Qed.

Definition limit_ordinal x:=
  is_ordinal x & inc emptyset x & (forall y, inc y x -> inc (succ_o y) x).

Lemma limit_ordinal_pr1: forall x, is_ordinal x ->
  (limit_ordinal x) = (nonempty x & x = union x).
Proof.
move=> x Bx.
move: (ordinal_irreflexive Bx) => ir.
 rewrite /limit_ordinal; apply iff_eq.
  move=> [_ [nex p]].
  split; first by exists emptyset.
  move: (limit_ordinal_pr0 Bx)=> [pq _]; case pq => //.
  move=> [y xy].
  have yx: (inc y x) by rewrite xy /succ_o; fprops.
  move: (p _ yx); rewrite -xy=> bad; contradiction.
move=> [nex xu]; split=>//.
split.
  have: emptyset <> x.
    by move=> h; rewrite -h in nex; elim (not_nonempty_empty nex).
  have: transitive_set emptyset by move=> t; case; case.
  move: (emptyset_sub_any x); apply Bx.
move=> y yx.
move: (elt_of_ordinal Bx yx)=> By.
case (ordinal_trichotomy (ordinal_succ By) Bx) =>//.
case.
  rewrite /succ_o; aw; case => h.
   move:((ordinal_transitive Bx yx) _ h); contradiction.
  rewrite -h in yx; contradiction.
move: (limit_ordinal_pr0 Bx)=> [ _ dj] h.
elim dj => //; by exists y.
Qed.

Lemma limit_ordinal_pr2: forall x, is_ordinal x ->
  x = emptyset \/ (exists y, x = succ_o y) \/ limit_ordinal x.
Proof.
move=> x ox.
case (emptyset_dichot x); first by intuition.
move=> new; right.
move: (limit_ordinal_pr0 ox) => [h _]; case: h; first by intuition.
move=> xu;rewrite (limit_ordinal_pr1 ox); intuition.
Qed.

Lemma ordinal_predecessor: forall y, is_ordinal y -> y = \opred (succ_o y).
Proof.
rewrite/succ_o; move=> y oy; set_extens t => ts.
  apply union_inc with y => //; fprops.
move: (union_exists ts) => [a [ta ax]].
move: ax; aw; case; last by move => <-.
move=> ay; apply (ordinal_transitive oy ay ta).
Qed.

Lemma ordinal_predecessor1: forall x, is_ordinal x ->
  (exists y, x = succ_o y) -> x = succ_o (\opred x).
Proof.
move=> x ox [y xs].
have yx: inc y x by rewrite xs /succ_o; fprops.
by rewrite xs - (ordinal_predecessor (elt_of_ordinal ox yx)).
Qed.

Definition infinite_o u := u \Eq (succ_o u).
Definition finite_o u := is_ordinal u & ~ (infinite_o u).

Lemma succ_injective_o: forall x y, is_ordinal x -> is_ordinal y ->
  (succ_o x) \Eq (succ_o y) = x \Eq y.
Proof.
move=> x y Bx By.
move: (ordinal_irreflexive Bx) (ordinal_irreflexive By) => h1 h2.
by rewrite (tack_on_injective_card2 h1 h2).
Qed.

Lemma infinite_o_increasing: forall x y, is_ordinal x -> is_ordinal y ->
  inc x y -> infinite_o x -> infinite_o y.
Proof.
rewrite /infinite_o; move=> x y xB yB xy.
move: (ordinal_irreflexive xB)(ordinal_irreflexive yB)
   (ordinal_transitive yB xy).
apply tack_on_injective_card3.
Qed.

Lemma finite_o_increasing: forall x y,
  inc x y -> finite_o y -> finite_o x.
Proof.
move=> x y xy [oy niy].
have ox: is_ordinal x by ord_tac0.
by split => //; dneg nix; apply (infinite_o_increasing ox oy xy).
Qed.

Lemma infinite_o_pr:
  forall x, is_ordinal x -> infinite_o (succ_o x) = infinite_o x.
Proof.
move=> x xB; apply (succ_injective_o xB (ordinal_succ xB)).
Qed.

Lemma finite_o_pr: forall x, finite_o x = finite_o (succ_o x).
Proof.
rewrite /finite_o;move=> x; apply iff_eq.
  move=> [p1 p2]; split; first by apply ordinal_succ.
  rewrite infinite_o_pr //.
move=> [p1 p2].
have bx: is_ordinal x by apply (elt_of_ordinal p1); rewrite /succ_o; fprops.
by split => //; rewrite -infinite_o_pr.
Qed.

Lemma limit_infinite: forall x, limit_ordinal x -> infinite_o x.
Proof.
move=> x xl.
have bx: is_ordinal x by move: xl => [ok _].
move: (ordinal_worder1 bx xl).
simpl; set A := least_ordinal limit_ordinal x.
move=> [oA [[_ [eA liA]] leA]].
suff p: (infinite_o A).
  case (ordinal_sub oA bx (leA _ bx xl)) => Ax; first by ue.
 apply (infinite_o_increasing oA bx Ax p).
move: (ordinal_irreflexive oA) => nAA.
set f:= fun z => Yo (inc z A) (tack_on z z) emptyset.
red; eqsym;exists (BL f (tack_on A A) A); ee; aw.
have q1: forall z, inc z (tack_on A A) -> inc (f z) A.
  by move=> u; aw; case => hu; rewrite /f ?hu ; Ytac0 => //; apply liA.
apply bl_bijective => //.
  move=> u v; aw; rewrite /f;case => uA; [ | rewrite uA]; Ytac0.
    case => vA; [ | rewrite vA]; Ytac0.
      move=> eq.
      have:inc u (tack_on u u) by fprops.
      have:inc v (tack_on v v) by fprops.
      rewrite eq - {1} eq; aw; case=>// uv; case => // vu.
      elim (ordinal_asymmetric oA uA vA vu uv).
    move=> bad; empty_tac1 u.
  case => vA; [ | rewrite vA]; Ytac0 => //.
  move=> bad; symmetry in bad; empty_tac1 v; move=> ->.
set z':= Zo A (fun z=> ~ (exists x0, inc x0 (tack_on A A) & f x0 = z)).
case (emptyset_dichot z') => nez.
  move=> y yA; apply exists_proof; move=> nex.
  empty_tac1 y; rewrite /z'; apply Z_inc=>//.
  by move=> [w q]; elim (nex w).
have alo': (forall a, inc a z' -> is_ordinal a).
  move => a; rewrite /z' Z_rw; move=> [aA _]; ord_tac.
move: (ordinal_intersection nez alo').
set B:= intersection z';move => iz'.
move: (iz');rewrite /z' Z_rw; move => [r1 r2].
move: (elt_of_ordinal oA r1) => oB.
case (emptyset_dichot B) => be.
  by elim r2; exists A; ee; rewrite /f Y_if_not_rw.
suff aux: (limit_ordinal B).
  move: ((leA _ oB aux) _ r1) => sab.
  by elim (ordinal_irreflexive oB).
rewrite limit_ordinal_pr1 //; split =>//.
move: (limit_ordinal_pr0 oB) => [ca _ ]; case ca =>//; move=> [y ta].
have yB: inc y B by rewrite ta /succ_o; fprops.
have yA: inc y A by apply (ordinal_transitive oA r1 yB).
have yAA: inc y (tack_on A A) by fprops.
have fy: f y = B by rewrite ta /f; Ytac0.
elim r2; ex_tac.
Qed.

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

Lemma Zermelo_ter: forall E, worder (worder_of E) & substrate (worder_of E) = E.
Proof.
move=> E.
rewrite /worder_of.
set p:= fun a => complement a (singleton (rep a)).
set (chain:= fun F => sub F (powerset E) & inc E F &
    (forall A, inc A F -> inc (p A) F)
    & (forall A, sub A F -> nonempty A -> inc (intersection A) F)).
set om := intersection _.
set (R:= fun p => intersection (Zo om (fun x => sub (singleton p) x))).
have omv: om = intersection (Zo (powerset (powerset E)) chain) by done.
set res := graph_on _ _.
set (m:= fun a => forall x, inc x om -> sub x a \/ sub a x).
have pe: p emptyset = emptyset.
  by empty_tac x xe; move: xe; rewrite /p; srw; case; case; case.
have sp: forall a, sub (p a) a by move=> t; rewrite /p; apply sub_complement.
have cp:chain (powerset E).
  split; fprops; split; first by apply powerset_inc; fprops.
  split; first by move=> A; aw; move=> AE; apply sub_trans with A.
  move=> A AP [x xA]; move: (AP _ xA); aw => xE.
  move=> t ti; apply xE; apply (intersection_forall ti xA).
have co :chain om.
 rewrite omv.
  have aux: (nonempty (Zo (powerset (powerset E)) chain)).
    by exists (powerset E); apply Z_inc; aw; fprops.
  rewrite /om; red; ee.
        by rewrite /om; apply intersection_sub; apply Z_inc; aw; fprops.
      apply intersection_inc=>//; move=>y; rewrite Z_rw/chain; aw; intuition.
    move=> A Ai; apply intersection_inc=>//.
    move=> y yi; move: (yi); rewrite Z_rw; move=> [_ [_[_ [q _]]]]; apply q.
    apply (intersection_forall Ai yi).
  move=> A sAi neA; apply intersection_inc=> //.
  move=> y yi; move: (yi); rewrite Z_rw; move=> [_ [_[_ [_ q]]]]; apply q=>//.
  move=>t tA; move: (sAi _ tA) => ti.
  by apply (intersection_forall ti yi).
move: (co)=> [sop [Eo [po io]]].
have cio: forall x, chain x -> sub om x.
  move=> x xc; rewrite / om; apply intersection_sub; apply Z_inc =>//.
  by aw; move:xc; rewrite /chain; intuition.
have am: om = Zo om m.
  apply extensionality; last by apply Z_sub.
  apply cio; red; ee.
        apply sub_trans with om; [by apply Z_sub| apply sop].
      by apply Z_inc=>//; move=> x xom; left;move: (sop _ xom); aw.
    move=> A; rewrite Z_rw; move=> [Aom mA].
    apply Z_inc; first by apply (po _ Aom).
    have aux: (sub om (Zo om (fun x=> sub x (p A) \/ sub A x))).
      apply cio; red; ee.
            by apply sub_trans with om; first by apply Z_sub.
          by apply Z_inc=>//; right; move: (sop _ Aom); aw.
        move => B; rewrite Z_rw; move => [Bom ors].
        apply Z_inc; first by apply (po _ Bom).
        case ors => orsi.
          left; apply sub_trans with B =>//; apply sp.
        case (mA _ (po _ Bom)) => aux; last by auto.
        case (inc_or_not (rep B) A)=> aux2.
          have BA: (sub B A).
            rewrite /p in aux2; move=> t tB.
            case (equal_or_not t (rep B)).
              by move=> ->.
            by move=> trB; apply aux; rewrite /p; srw; aw.
          have: (B = A) by apply extensionality.
          by move=> ->; intuition.
        right; move=> t tA; rewrite /p; srw; aw.
        split; [ by apply orsi| dneg trB; ue].
      move=> B sB neB; apply Z_inc.
        apply io =>//; apply: sub_trans; [eexact sB| apply Z_sub].
      case (p_or_not_p (exists x, inc x B & sub x (p A))) => aux.
        move: aux=> [x [xB xp]]; left; move=> t ti; apply xp.
        apply (intersection_forall ti xB).
      right; move=> t tA; apply intersection_inc=>//.
      move=> y yB; move: (sB _ yB); rewrite Z_rw; move=> [yom ors].
      case ors; last by apply.
      by move => sy; elim aux; ex_tac.
    move=> x xom; case (mA _ xom) => hyp.
      move: (aux _ xom); rewrite Z_rw; move=> [_ xpA].
      case xpA=>xpB; first by auto.
      have Ax: (A = x) by apply extensionality.
      rewrite Ax; right; apply sp.
    by right; apply sub_trans with A=>//; apply sp.
  move=> A sAZ neA; apply Z_inc.
    apply io =>//; apply sub_trans with (Zo om m) =>//; apply Z_sub.
  move=> x xom.
  case (p_or_not_p (exists y, inc y A & sub y x)) => hyp.
    move: hyp=> [y [yA yx]]; right; move => t ti.
    apply yx; apply (intersection_forall ti yA).
  left; move=> t tx; apply intersection_inc=>//.
  move=> y yA; move: (sAZ _ yA); rewrite Z_rw; move=> [yom my].
  case (my _ xom);[ by apply | move=> yx; elim hyp; ex_tac; apply Z_sub].
have st: forall a b, inc a om -> inc b om -> sub a b \/ sub b a.
  move=> a b; rewrite {2} am Z_rw; move=> aom [bom ba]; apply (ba _ aom).
set d:= fun p => intersection (Zo om (fun x => sub p x)).
have dpo: forall q, sub q E -> inc (d q) om.
  by move=> q qE; rewrite /d; apply io;[ apply Z_sub| exists E;apply Z_inc].
have pdp: forall q, sub q E -> sub q (d q).
  rewrite /d=> q qE t tq; apply intersection_inc.
    by exists E; apply Z_inc.
  by move => y; rewrite Z_rw; move=>[_]; apply.
have dpq: forall q r, inc r om -> sub q r -> sub q E-> sub (d q) r.
  by rewrite /d=> q r0 rom qr qE; apply intersection_sub; apply Z_inc.
have rdq: forall q, sub q E -> nonempty q -> inc (rep (d q)) q.
  move=> q qE neq; case (inc_or_not (rep (d q)) q)=>// ni.
  have aux: (sub q (p (d q))).
    by rewrite /p=> t tq; srw; aw; split; [ apply (pdp _ qE)| dneg tr; ue].
  move: (dpq _ _ (po _ (dpo _ qE)) aux qE).
  rewrite /p; case (emptyset_dichot (d q)).
    move=> dqe; rewrite dqe pe in aux.
    by move: neq=> [t tq]; elim (emptyset_pr (x:= t)); apply aux.
  move=> ned; move: (nonempty_rep ned) => rd dc; move: (dc _ rd); srw.
  aw; intuition.
have qdp: forall q r, inc r om -> sub q r -> inc (rep r) q -> r = d q.
  move => q r rom qr rq.
  have spE: sub q E.
    by apply sub_trans with r=>//; apply powerset_sub; apply sop.
  move: (dpq _ _ rom qr spE) => sdqr.
  case (st _ _ (dpo _ spE) (po _ rom)) => ch.
    move: (pdp _ spE) => qdp.
    have:(inc (rep r) (p r)) by apply ch; apply qdp.
    rewrite /p; srw; aw; intuition.
  apply extensionality =>// t tr.
  case (equal_or_not t (rep r)).
    by move=> ->; apply (pdp _ spE).
  by move=> tnr; apply ch; rewrite /p; srw; aw; auto.
have Rp: forall x, inc x E ->
    (inc (R x) om & inc x (R x) & rep (R x) = x).
  rewrite /R=> x xE.
  have p1: sub (singleton x) E by apply sub_singleton.
  move: (pdp _ p1) => p2; ee; first by apply dpo.
  have nesi: (nonempty (singleton x)) by fprops.
  by move: (rdq _ p1 nesi); aw.
have Ri:forall x y, inc x E -> inc y E -> R x = R y -> x = y.
  move=> x y xE yE; move: (Rp _ xE)(Rp _ yE).
  by move=> [_ [_ p1]][_[_ p2]] p3; rewrite -p3 in p2; rewrite -p1 -p2.
have Rrq: forall q, inc q om -> nonempty q -> R (rep q) = q.
  move=> a qom neq; rewrite /R; symmetry; apply qdp =>//.
  by move=> t; aw; move=> ->; apply nonempty_rep.
  fprops.
have sRR: forall x y, inc x E -> inc y E -> inc x (R y) -> (sub (R x) (R y)).
  move=> x y xE yE xRy.
  move: (Rp _ xE)(Rp _ yE) => [Rom [xRx rR]] [Rom' [yRy rR']].
 case (st _ _ Rom Rom') =>// hyp.
  have p1:(sub (doubleton x y) (R y)).
    by move=> t td; case (doubleton_or td)=>->.
  have p2: (sub (doubleton x y) (R x)) by apply sub_trans with (R y).
  have p3: (inc (rep (R x)) (doubleton x y)) by rewrite rR; fprops.
  have p4: (inc (rep (R y)) (doubleton x y)) by rewrite rR'; fprops.
  move: (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4).
  move=> -> ->; fprops.
have or:order res.
  rewrite /res; apply order_from_rel1.
      by move=> x y z /= xy yz; apply sub_trans with (R y).
    by move=> u v uE vE vu uv; apply Ri=>//; apply extensionality.
  move => u ue; fprops.
have sr: substrate res = E.
  rewrite /res substrate_graph_on //; move => u ue; fprops.
split=>//;split=>//.
move=> x xsr nex.
rewrite sr in xsr.
move: (rdq _ xsr nex) => rdx.
exists (rep (d x)); split.
  by aw;rewrite sr.
aw; move=> a ax; aw; last by ue.
rewrite /res /gle graph_on_rw1;ee.
apply sRR; try apply xsr=>//.
move: ((pdp _ xsr) _ ax)=> adx.
have ne: (nonempty (d x)) by exists a.
rewrite Rrq //.
by apply dpo.
Qed.

Definition cardinal_of x :=
  (least_ordinal (equipotent x) (ordinal (worder_of x))).

Definition cardinalVp x y :=
  is_ordinal y & x \Eq y &
  (forall z, is_ordinal z -> x \Eq z -> sub y z).

Lemma cardinalV_unique: forall x y z,
  cardinalVp x y -> cardinalVp x z -> y = z.
Proof.
move=> x y z [By [exy p1]] [Bz [exz p2]].
by apply extensionality; [ apply p1 | apply p2 ].
Qed.

Lemma cardinalV_exists: forall x, cardinalVp x (cardinal_of x).
Proof.
move=> x.
move: (Zermelo_ter x)=> [wor sr].
move: (ordinal_isomorphism_exists wor) => [or oi].
set f :=(transfinite_defined (worder_of x) target) in or oi.
have extf: x \Eq (ordinal (worder_of x)).
  move : oi => [_ [_ [bf [sf [tf ff]]]]]; exists f; ee; ue.
apply (ordinal_worder1 or extf).
Qed.

Module Type CardinalSig.
Parameter cardinal : Set -> Set.
Axiom cardinalE: cardinal = cardinal_of.
End CardinalSig.

Module Cardinal: CardinalSig.
Definition cardinal := cardinal_of.
Lemma cardinalE: cardinal = cardinal_of. Proof. by []. Qed.
End Cardinal.

Notation cardinal := Cardinal.cardinal.

Lemma cardinalV_pr: forall x,
   is_ordinal (cardinal x) & x \Eq (cardinal x) &
  (forall z, is_ordinal z -> x \Eq z -> sub (cardinal x) z).
Proof.
move=> x; rewrite Cardinal.cardinalE; apply cardinalV_exists.
Qed.

Definition is_cardinal x:=
 is_ordinal x & (forall z, is_ordinal z -> x \Eq z -> sub x z).

Lemma cardinal_of_cardinal: forall x, is_cardinal x -> cardinal x = x.
Proof.
move=> x [cx1 cx2].
have aux: cardinalVp x (cardinal x) by apply cardinalV_pr.
have aux': cardinalVp x x by red; ee.
apply (cardinalV_unique aux aux').
Qed.

Lemma cardinal_cardinal: forall x, is_cardinal (cardinal x).
Proof.
move=> x; move: (cardinalV_pr x) => [p1 [p2 p3]].
split => //; move=> z Bz ez; apply p3 => //; eqtrans (cardinal x).
Qed.

Lemma cardinal_ordinal: forall x, is_cardinal x -> is_ordinal x.
Proof. by move=> x [ox _]. Qed.

Hint Resolve cardinal_cardinal: fprops.

Lemma double_cardinal: forall x, cardinal (cardinal x) = cardinal x.
Proof. move=> x; apply cardinal_of_cardinal; fprops. Qed.

Lemma cardinal_pr0: forall x, x \Eq (cardinal x).
Proof.
by move=> x; move: (cardinalV_pr x)=> [_ [ok _]].
Qed.

Lemma cardinal_pr: forall x, (cardinal x) \Eq x.
Proof. by move=> x;eqsym; apply cardinal_pr0. Qed.

Hint Resolve cardinal_pr0 cardinal_pr: fprops.

Theorem cardinal_equipotent: forall x y,
   (cardinal x = cardinal y) = (x \Eq y).
Proof.
move=> x y.
apply iff_eq => h.
   eqtrans (cardinal x); rewrite h; eqsym; fprops.
move: (cardinalV_pr x) (cardinalV_pr y) => [Bx [exo lx]][By [eyp ly]].
apply extensionality.
apply lx =>//; eqtrans y.
by apply ly =>//; eqtrans x; eqsym.
Qed.

Hint Rewrite cardinal_equipotent: aw.

Lemma is_cardinal_pr: forall x,
  is_cardinal x = (is_ordinal x & forall z, inc z x -> ~ (x \Eq z)).
Proof.
move=> x; rewrite /is_cardinal; apply iff_eq; move=> [bx h]; ee.
  move => z zx ne; move: ((h _ (elt_of_ordinal bx zx) ne) _ zx).
  apply (ordinal_decent bx zx).
move=> z bz exz.
case: (ordinal_trichotomy bz bx) => ty; first by elim (h _ ty).
case ty; first by apply (ordinal_transitive bz).
move=> ->; fprops.
Qed.

Definition card_zero := emptyset.
Definition card_one := singleton emptyset.
Definition card_two := doubleton emptyset (singleton emptyset).

Notation "0 'c'" := card_zero.
Notation "1 'c'" := card_one.
Notation "2 'c'" := card_two.

Lemma succ_o_zero: succ_o 0c = 1c.
Proof.
rewrite /succ_o /tack_on /0c /1c.
set_extens z; rewrite union2_rw; last by intuition.
case => //; case; case.
Qed.

Lemma succ_o_one: succ_o 1c = 2c.
Proof.
rewrite /succ_o /tack_on /2c /1c.
set_extens z; rewrite union2_rw doubleton_rw; aw.
Qed.

Lemma ordinal_zero: is_ordinal 0c.
Proof.
move=> y yx ty ney; elim ney.
apply extensionality=>//; apply emptyset_sub_any.
Qed.

Lemma ordinal_one: is_ordinal 1c.
Proof. rewrite - succ_o_zero; apply ordinal_succ; apply ordinal_zero. Qed.

Lemma ordinal_two: is_ordinal 2c.
Proof. rewrite - succ_o_one; apply ordinal_succ; apply ordinal_one. Qed.

Lemma equipotent_to_emptyset:
  forall x, x \Eq emptyset -> x = emptyset.
Proof.
move=> x [y [[[fy _] suy] [sy ty]]].
apply is_emptyset; move=> z zx; empty_tac1 (W z y).
apply inc_W_target =>//; ue.
Qed.

Lemma finite_zero: finite_o 0c.
Proof.
split; first by apply ordinal_zero.
move=> h; move: (equipotent_symmetric h); rewrite /card_zero=> h'.
move: (equipotent_to_emptyset h') => h''.
have bad: inc emptyset emptyset. rewrite -{2} h'' /succ_o; fprops.
elim (emptyset_pr bad).
Qed.

Lemma finite_one: finite_o 1c.
Proof. rewrite -succ_o_zero; rewrite - finite_o_pr; apply finite_zero. Qed.

Lemma finite_two: finite_o 2c.
Proof. rewrite -succ_o_one; rewrite - finite_o_pr; apply finite_one. Qed.

Lemma finite_succ : forall x,
  finite_o x = (x = emptyset \/ (exists y, finite_o y & x = succ_o y)).
Proof.
move=> x; apply iff_eq.
  move => fx; move: (fx) => [ox nix].
  case (limit_ordinal_pr2 ox); first by intuition.
  case.
    move=> [y xK]; rewrite xK; right; exists y; ee.
    by move: fx; rewrite xK - finite_o_pr.
  move=> h; elim nix;apply (limit_infinite h).
case.
  move => ->; apply finite_zero.
by move=> [y [fy]] ->; rewrite -finite_o_pr.
Qed.

Lemma finite_cardinal_pr: forall x, finite_o x ->
  is_cardinal (succ_o x).
Proof.
rewrite /finite_o /infinite_o /succ_o.
move=> x [ox nix]; rewrite is_cardinal_pr; split; first by apply ordinal_succ.
move=> z zo.
dneg aux1; eqtrans z; last by eqsym.
have zx: (sub z x).
  move: zo;rewrite /succ_o; aw.
  case; [apply (ordinal_transitive ox) | move=> ->; fprops].
move: (ordinal_irreflexive ox) => xx.
move: aux1 => [g [[[fg injg] sjg] [sg tg]]].
set (f:= fun z => W z g).
have p1: (forall t, inc t x -> inc (f t) z).
   rewrite -tg /f=>t tx; apply inc_W_target => //; rewrite sg; fprops.
have p2:(forall u v, inc u x -> inc v x -> f u = f v -> u = v).
  rewrite /f => u v uE vE; apply injg; rewrite sg; fprops.
apply (Cantor_Bernstein1 zx p1 p2).
Qed.

Lemma cardinal0: is_cardinal 0c.
Proof.
rewrite /card_zero is_cardinal_pr; split; first by apply ordinal_zero.
move=> z;case; case.
Qed.

Lemma cardinal1: is_cardinal 1c.
Proof. rewrite -succ_o_zero; apply finite_cardinal_pr; apply finite_zero. Qed.

Lemma cardinal2: is_cardinal 2c.
Proof. rewrite -succ_o_one; apply finite_cardinal_pr; apply finite_one. Qed.

Lemma finite_cardinal_pr1: forall x, finite_o x -> is_cardinal x.
Proof.
move=> x; rewrite finite_succ; case.
  move => ->; apply cardinal0.
by move=> [y [yF]] ->; apply finite_cardinal_pr.
Qed.

Lemma infinite_pr1: forall y z, is_cardinal z -> infinite_o z ->
  z = succ_o y -> False.
Proof.
move=> y z; rewrite is_cardinal_pr; move=> [c1 c2] Viz zyy.
have yz: (inc y z) by rewrite zyy /succ_o; fprops.
elim (c2 _ yz); eqsym.
rewrite zyy in Viz.
move: (elt_of_ordinal c1 yz) => By.
by move: Viz; rewrite (infinite_o_pr By) /infinite_o -zyy.
Qed.

Definition finite_c := finite_o.
Definition infinite_c a := is_cardinal a & infinite_o a.
Definition finite_set E := finite_c (cardinal E).
Definition infinite_set E := infinite_o (cardinal E).

Lemma infinite_dichot1 : forall x, finite_c x -> infinite_c x -> False.
Proof. move=> x; move=> [_ pa][_ pb]; contradiction. Qed.

Lemma infinite_dichot2 :
  forall x, finite_c (cardinal x) -> infinite_set x -> False.
Proof. move=> x p1 p2; apply (infinite_dichot1 p1); split; ee. Qed.

Lemma finite_cardinal_pr2: forall x, finite_c x -> is_cardinal x.
Proof. by move=> x; apply finite_cardinal_pr1. Qed.

Lemma infinite_nonempty: forall x, infinite_c x -> nonempty x.
Proof.
move=> x ic; case (emptyset_dichot x) => //.
move=> h; rewrite h in ic.
elim (infinite_dichot1 finite_zero ic).
Qed.

Hint Resolve finite_cardinal_pr2: fprops.

Definition succ x := cardinal (succ_o x).

Lemma cardinal_irreflexive : forall x, is_cardinal x -> ~ (inc x x).
Proof. move=> x [ox _]; apply (ordinal_irreflexive ox). Qed.

Theorem succ_injective1: forall a b, is_cardinal a -> is_cardinal b ->
   succ a = succ b -> a = b.
Proof.
move=> a b ca cb; rewrite /succ/succ_o; aw.
move: (cardinal_cardinal a) (cardinal_cardinal b) => cca ccb.
rewrite tack_on_injective_card2//.
    rewrite - cardinal_equipotent; rewrite ! cardinal_of_cardinal //.
  apply cardinal_irreflexive => //.
apply cardinal_irreflexive => //.
Qed.

Lemma cardinal_succ_pr: forall a b, ~ (inc b a) ->
  cardinal (tack_on a b) = succ (cardinal a).
Proof.
move=> a b bna; rewrite /succ /succ_o; aw.
rewrite tack_on_injective_card2 //; first by fprops.
apply cardinal_irreflexive; fprops.
Qed.

Lemma cardinal_succ_pr1: forall a b,
  cardinal (tack_on (complement a (singleton b)) b) =
  succ (cardinal (complement a (singleton b))).
Proof.
move=> a b; rewrite cardinal_succ_pr //.
apply not_inc_complement_singleton.
Qed.

Lemma cardinal_succ_pr2: forall a b, inc b a ->
  cardinal a = succ (cardinal (complement a (singleton b))).
Proof.
move=> a b ba.
have p: (tack_on (complement a (singleton b)) b) = a.
  set_extens t; aw; srw; aw.
    case; [intuition | move=> -> //].
  move=> ta; case (equal_or_not t b); intuition.
rewrite -{1} p; apply cardinal_succ_pr1.
Qed.

Lemma infinite_set_pr: forall a b, inc b a ->
  a \Eq (complement a (singleton b)) ->
  infinite_set a.
Proof.
move=> a b ba eq.
rewrite -cardinal_equipotent in eq.
red; red. rewrite -cardinal_equipotent double_cardinal.
move: (cardinal_succ_pr2 ba); rewrite -eq /succ //.
Qed.

Lemma infinite_set_pr1: forall a b, inc b a ->
  a \Eq (complement a (singleton b)) ->
  infinite_set (complement a (singleton b)).
Proof.
move=> a b ab => h.
move: (infinite_set_pr ab h).
rewrite /infinite_set. rewrite -cardinal_equipotent in h.
by rewrite -h.
Qed.

Lemma infinite_set_pr2: forall x, infinite_o x -> ~(inc x x) -> infinite_set x.
Proof.
move=> x; rewrite /infinite_o/succ_o => eq1 eq2.
set (a:= (tack_on x x)).
move: (equipotent_symmetric eq1) => eq3.
have eq4: x = complement a (singleton x).
  rewrite /a;set_extens t; srw; aw => h.
    split; [ auto |by dneg w ; rewrite -{1} w].
  case h; case; [auto | move=> p1 p2; contradiction].
rewrite eq4; apply infinite_set_pr1; [ rewrite /a; fprops | ue ].
Qed.

Lemma nat_infinite_set: infinite_set nat.
Proof.
have zn: inc (Ro 0) nat by apply R_inc.
apply (infinite_set_pr zn).
set f:= corresp nat (complement nat (singleton (Ro 0))) (gacreate S).
have gf: graph f = (gacreate S) by rewrite /f; aw.
have p0: fgraph (gacreate S).
  split.
    move=> t; rewrite /gacreate IM_rw; move=> [a] <-; fprops.
  move=> x y; rewrite /gacreate IM_rw IM_rw.
  move=> [a J1][b J2] sp; rewrite -J1 -J2 in sp; awi sp.
  by rewrite -J1 -J2 sp; rewrite (R_inj sp).
have p1: is_graph (gacreate S) by fprops.
have p2:nat = domain (gacreate S).
  set_extens t; dw.
    move=> tn; exists (Ro (S (Bo tn))).
    rewrite /gacreate IM_rw; exists (Bo tn); by rewrite B_eq.
  move=> [y]; rewrite /gacreate IM_rw.
  move=> [a Je]; rewrite -(pr1_def Je); apply R_inc.
have p3: (range (gacreate S))= (complement nat (singleton (Ro 0))).
  set_extens t; dw; srw; aw.
    move=>[x]; rewrite /gacreate IM_rw; move=> [a Jeq].
    rewrite -(pr2_def Jeq); ee; first by apply R_inc.
    move=> h; move:(R_inj h); discriminate.
  move=> [tn to].
  have [w wp]: exists w:nat, t = Ro w by exists (Bo tn); rewrite (B_eq tn).
  rewrite wp in to |- *; clear wp.
  have: w <> 0 by dneg xx; ue.
  case w; first by intuition.
  move => n _; exists (Ro n);rewrite /gacreate IM_rw; exists n =>//.
have ff: is_function f.
  apply is_function_pr =>//; rewrite p3; fprops.
have sf: surjection f by apply surjective_pr4 =>//;rewrite /f; aw.
exists f; ee.
  split;ee.
    apply injective_pr_bis =>//.
    move=> x x' y; rewrite /related gf/gacreate IM_rw IM_rw.
    move=> [a J1][b J2].
    move: (pr2_def J1)(pr2_def J2)=> r3 r4.
    rewrite -r4 in r3; move: (R_inj r3)=> r5.
    by rewrite -(pr1_def J1) - (pr1_def J2) (eq_add_S _ _ r5).
rewrite /f; aw.
rewrite /f; aw.
Qed.

Definition omega0 := least_ordinal infinite_o (cardinal nat).

Lemma omega0_pr:
   is_ordinal omega0 & infinite_o omega0 &
   (forall z, is_ordinal z -> infinite_o z -> sub omega0 z).
Proof.
have p1: is_ordinal (cardinal nat).
  by move: (cardinal_cardinal nat) => [ok _].
by move: (ordinal_worder1 p1 nat_infinite_set).
Qed.

Lemma omega0_ordinal: is_ordinal omega0.
Proof. by move: omega0_pr => [h _]. Qed.

Lemma omega0_infinite: infinite_o omega0.
Proof. by move: omega0_pr => [_ [h _]]. Qed.

Lemma omega0_pr1: forall x, is_ordinal x ->
  (infinite_o x = sub omega0 x).
Proof.
move=> x Bx; apply iff_eq.
 by move: omega0_pr => [_ [_ h]]; apply h.
move: omega0_infinite omega0_ordinal => bi oB sBx.
case (ordinal_sub oB Bx sBx); first by move => <- //.
move=> h; apply (infinite_o_increasing oB Bx h bi).
Qed.

Lemma omega0_pr2: forall x, inc x omega0 = finite_o x.
Proof.
move: omega0_ordinal => oB.
move=> x; apply iff_eq=> xB.
  move: (elt_of_ordinal oB xB) => xo.
  split=>//; move=> h.
  rewrite (omega0_pr1 xo) in h.
  elim (ordinal_irreflexive xo (h _ xB)).
move: xB => [xo nifx].
case (ordinal_le_total_order2 oB xo) => //.
rewrite -(omega0_pr1 xo) => h; contradiction.
Qed.

Lemma omega0_cardinal: is_cardinal omega0.
Proof.
red. ee. apply omega0_ordinal.
move=> e oe ez; rewrite -omega0_pr1 //.
move: omega0_infinite; rewrite /infinite_o => aux.
eqtrans (succ_o omega0). by eqtrans omega0; eqsym.
rewrite succ_injective_o //; apply omega0_ordinal.
Qed.

Lemma omega0_limit: omega0 = \opred omega0.
Proof.
move: (limit_ordinal_pr0 omega0_ordinal) => [h _]; case h=>//.
move=> [y yB].
have yiB: inc y omega0 by rewrite yB/ succ_o; fprops.
move: yiB; rewrite omega0_pr2 finite_o_pr -yB; move => [_ Of].
by elim Of; apply omega0_infinite.
Qed.

Lemma omega0_limit1: limit_ordinal omega0.
Proof.
rewrite limit_ordinal_pr1; last by apply omega0_ordinal.
split; last by apply omega0_limit.
exists card_zero; rewrite omega0_pr2; apply finite_zero.
Qed.

Lemma omega0_limit2: forall x, limit_ordinal x -> sub omega0 x.
Proof.
move=> x h.
have Bx: (is_ordinal x) by move: h=> [bo _].
rewrite -(omega0_pr1 Bx); apply (limit_infinite h).
Qed.

Lemma infinite_card_limit1: forall x, infinite_c x -> \opred x = x.
Proof.
move => x [p1 p2].
move: (limit_ordinal_pr0 (cardinal_ordinal p1)) => [p3 _].
case p3 => //.
move=> [y h]; elim (infinite_pr1 p1 p2 h).
Qed.

Lemma infinite_card_limit2: forall x, infinite_c x -> limit_ordinal x.
Proof.
move => x ic; move: (ic) => [p1 p2].
rewrite (limit_ordinal_pr1 (cardinal_ordinal p1)).
split; last by symmetry;apply infinite_card_limit1.
by apply infinite_nonempty.
Qed.

Lemma omega_limit3: forall x, infinite_c x -> sub omega0 x.
Proof.
by move=> x h; apply omega0_limit2; apply infinite_card_limit2.
Qed.

End Bordinal.

Export Bordinal.

Module Cardinal.