Library sset7

Theory of Sets EIII-3 Equipotents Sets. Cardinals

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


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

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

Module Bordinal.

Ordinals

We start with some properties of a set; ordinal_oa and ordinal_o are orderings

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 trans_dec_set X := transitive_set X /\ decent_set X.
Definition asymmetric_set E :=
  forall x y, inc x E -> inc y E -> inc x y -> inc y x -> False.
Definition ordinal_oa := graph_on (fun a b => inc a b \/ a = b).
Definition ordinal_o := sub_order.
Definition succ_o x := x +s1 x.

Lemma transitive_setU x: (alls x transitive_set)
  -> transitive_set (union x).
Proof.
move=> alt a au t ta; move: (setU_hi au)=> [y ay yx].
move: (( (alt _ yx) _ ay) _ ta) => ty; union_tac.
Qed.

Lemma trans_dec_setU x: (alls x trans_dec_set)
  -> trans_dec_set (union x).
Proof.
move=> alt; split.
  apply: transitive_setU => y yx; exact (proj1 (alt _ yx)).
by move=> a /setU_hi [y ay yx] aa; case: ((proj2 (alt _ yx)) _ ay).
Qed.

Lemma trans_dec_setI x:
  (alls x trans_dec_set) -> trans_dec_set (intersection x).
Proof.
case: (emptyset_dichot x).
  by move => -> _; rewrite setI_0; split => t /in_set0.
move=> nea alt; split.
  move=> a au t ta; apply: (setI_i nea).
  move=> y yx; apply: ((proj1 (alt _ yx)) _ (setI_hi au yx)) =>//.
move=> a au aa; move: nea => [y yx].
by apply: ((proj2 (alt _ yx)) _ (setI_hi au yx)).
Qed.

Lemma succ_i x: inc x (succ_o x).
Proof. by apply/setU1_P; right. Qed.

Hint Resolve succ_i: fprops.

Lemma trans_dec_succ y:
  trans_dec_set y -> trans_dec_set (succ_o y).
Proof.
move => [pa pb]; split.
  move => z /setU1_P; case.
    by move => zy t tz; move: ((pa _ zy) _ tz) => ty; apply/setU1_P; left.
  by move => -> t ty; apply/setU1_P; left.
by move => z zs zz; case: (pb z) => //; case /setU1_P: zs => // <-.
Qed.

Definition of an ordinal; set such sets are transitive and decent

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

Notation "f =1o g" := (forall x, ordinalp x -> f x = g x)
  (at level 70, format "'[hv' f '/ ' =1o g ']'", no associativity).
Definition ordinal_fam g := allf g ordinalp.
Definition ordinal_set E := alls E ordinalp.

Lemma ordinal_trans_dec x: ordinalp x -> trans_dec_set x.
Proof.
move=> ox.
set y := Zo (powerset x) trans_dec_set.
set t := union y.
have: trans_dec_set t by apply: trans_dec_setU=> z /Zo_hi.
case: (equal_or_not t x); first by move=> ->.
move=> ntx tct; move: (trans_dec_succ tct) => tcst.
have sux: sub t x by apply: setU_s2; move =>z /Zo_P [] /setP_P.
move: (ox _ sux (proj1 tct) ntx)=> ux.
case: ((proj2 tcst) _ (succ_i t)).
apply: (setU_i (succ_i t)); apply: Zo_i => //.
by apply/setP_P => s /setU1_P; case; [apply: sux | move=> ->].
Qed.

Lemma ordinal_transitive x: ordinalp x -> transitive_set x.
Proof. by move => ox; move: (ordinal_trans_dec ox)=> []. Qed.

Lemma ordinal_decent x: ordinalp x -> decent_set x.
Proof. by move => ox; move: (ordinal_trans_dec ox)=> []. Qed.

Lemma ordinal_irreflexive x: ordinalp x -> ~ (inc x x).
Proof. by move=> ox xx; case: (ordinal_decent ox xx). Qed.

For ordinals inc is the same as strict_sub

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

Lemma ordinal_sub2 x y: ordinalp y ->
  inc x y -> ssub x y.
Proof.
move=> /ordinal_trans_dec [ty dy xy]; split; first by apply: ty.
by move: (dy _ xy) => ab; dneg ac; rewrite {2} ac.
Qed.

Lemma ordinal_sub3 x y: ordinalp y ->
  inc x (succ_o y) -> sub x y.
Proof.
by move => /ordinal_transitive yb /setU1_P;case;[ apply: yb | move => ->].
Qed.

Lemma ordinal_sub4P x y: ordinalp x -> ordinalp y ->
  (sub x y <-> inc x (succ_o y)).
Proof.
move=> xb yb; split; last by apply: ordinal_sub3.
by case /(ordinal_sub xb yb) => a; apply/setU1_P; [right | left].
Qed.

The intersection of a set of ordinal is in the set; we deduce the trichotomy property, which says that sub is a total ordering for ordinals

Lemma ordinal_setI x: nonempty x -> ordinal_set x ->
   inc (intersection x) x.
Proof.
move=> nex alo; ex_middle nux.
have [pa pb]: (trans_dec_set (intersection x)).
  apply: trans_dec_setI =>//.
  by move=> y yx; move: (ordinal_trans_dec (alo _ yx)).
suff: inc (intersection x) (intersection x) by move => iii; case: (pb _ iii).
apply: setI_i =>// a ax; apply: (alo _ ax) => //.
  by move=>t tix; apply: (setI_hi tix ax).
by dneg xx; rewrite xx.
Qed.

Lemma ordinal_trichotomy x y:
  ordinalp x -> ordinalp y ->
  [\/ inc x y, inc y x | x = y].
Proof.
move=> ox oy.
have aux: (ordinal_set (doubleton x y)) by move=> a /set2_P [] ->//.
case /set2_P: (ordinal_setI (set2_ne x y) aux).
  move/setI2id_Pl => h;case: (ordinal_sub ox oy h) => p; in_TP4.
move/setI2id_Pr => h;case: (ordinal_sub oy ox h); in_TP4.
Qed.

X is an ordinal if it is transitive and its elements are ordinals; or if it is the successor of an ordinal

Lemma ordinal_pr x: transitive_set x -> ordinal_set x ->
  ordinalp x.
Proof.
move=> tx alo y sys ty nyx.
move: (setC_ne (conj sys nyx)) =>[z /setC_P [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 //;case:nzy; [ by apply: (ty _ ty')| ue].
case: (equal_or_not y z); first by move=> ->.
move=> yz; apply: (tx _ zx _ (oz _ zy ty yz)).
Qed.

Lemma OS_succ x: ordinalp x -> ordinalp (succ_o x).
Proof.
move=> ox y ytx tsy yntxx.
case: (equal_or_not y x) => yx; first by rewrite yx; fprops.
apply/setU1_P;left; apply: ox => //.
move=> t ty; move: (ytx _ ty); case /setU1_P => //.
move=> tx; case: yntxx; apply: extensionality=>// => s; case /setU1_P => sx.
  by rewrite tx in ty; move: (tsy _ ty); apply.
by rewrite sx - tx.
Qed.

Hint Resolve OS_succ : fprops.

Any element of an ordinal is an ordinal, in particular, if the successor of x is an ordinal, so is x; and no set contains all ordinals

Lemma ordinal_hi x y: ordinalp x -> inc y x -> ordinalp y.
Proof.
move=> ox yx.
set t:= union (Zo(powerset x) (fun y=> transitive_set y /\ ordinal_set y)).
have tp: ordinal_set t by move => z /setU_P [v zv /Zo_hi [_]]; apply.
have ot: ordinalp t.
  by apply: ordinal_pr=> //;apply: transitive_setU; move=> t' /Zo_hi [pb _].
case: (ordinal_trichotomy ox ot); last by move => tx;apply: tp; ue.
  move=> /setU_P [v xv /Zo_P [] /setP_P aux _].
  case: (ordinal_irreflexive ox (aux _ xv)).
move => tx.
case: (ordinal_irreflexive ot).
apply: (@setU_i _ (t +s1 t)); [fprops | apply: Zo_i ].
  move: (ordinal_transitive ox)=> trx.
  by apply/setP_P => s; case/setU1_P; [ apply: trx | move=> ->].
split; first by apply: (ordinal_transitive (OS_succ ot)).
by move=> u /setU1_P; case; [ apply: tp |move=> ->// ].
Qed.

Lemma ordinal_set_ordinal x: ordinalp x -> ordinal_set x.
Proof. move => ox t ot; exact:(ordinal_hi ox ot). Qed.

Lemma OS_succr x: ordinalp (succ_o x) -> ordinalp x.
Proof. move=> os ; apply: (ordinal_hi os); fprops. Qed.

Ltac ord_tac0 :=
 match goal with
  | h1: ordinalp ?a, h2: inc ?b ?a |- ordinalp ?b =>
    apply: (ordinal_hi h1 h2)
  | h1: ordinalp ?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, ordinalp a -> inc a x).
Proof.
move=> [x xp]; set (y := Zo x ordinalp).
have osy: ordinal_set y by move => t /Zo_hi.
have oo: forall a, ordinalp a -> inc a y.
  by move => a oa; apply: Zo_i => //; apply: xp.
have yo: ordinalp y.
  apply: ordinal_pr => // a ay b ba.
  apply: (oo _ (ordinal_hi (osy _ ay) ba)).
case: (ordinal_irreflexive yo (oo _ yo)).
Qed.

Since an ordinal is irreflexive it is asymmetric, and the successor function is injective

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

Lemma ord_succ_inj : { when ordinalp &, injective succ_o }.
Proof.
move=> a b oa ob eq.
have : inc a (succ_o b) by rewrite -eq; fprops.
case /setU1_P => // ab.
have : inc b (succ_o a) by rewrite eq; fprops.
case /setU1_P => // ba.
case: (ordinal_irreflexive oa (ordinal_transitive oa ba ab)).
Qed.

Lemma ordo_leP a b c:
  gle (ordinal_o a) b c <-> [/\ inc b a, inc c a & sub b c].
Proof. apply: sub_gleP. Qed.

Lemma ordo_ltP a b c: ordinalp c -> inc a c -> inc b c ->
   (glt (ordinal_o c) a b <-> inc a b).
Proof.
move=> oc ac bc.
move: (ordinal_hi oc bc) => ob.
split.
  move => [] /ordo_leP [h1 h2 h3] h4.
  by case: (ordinal_sub (ordinal_hi oc ac) ob h3).
move=> ab; move: (ordinal_sub2 ob ab)=> [h1 h2].
by split => //;apply /ordo_leP.
Qed.

If p x holds for some ordinal, then p holds for a least ordinal (for sub)

Definition least_ordinal (p: property) x:= intersection (Zo (succ_o x) p).

Lemma least_ordinal1 x (p: property) (y:= least_ordinal p x) :
  ordinalp x -> (p x) ->
    [/\ ordinalp y, p y & forall z, ordinalp z -> p z -> sub y z].
Proof.
move=> bx px.
set (t:= Zo (succ_o x) p).
have xt: inc x t by apply /Zo_i; fprops.
have net: nonempty t by exists x.
have alo: (ordinal_set t) by move :(OS_succ bx) => aux a /Zo_S ak; ord_tac0.
have h:= (ordinal_setI net alo).
split;[by apply: alo | by move: h => /Zo_hi |].
have sxt: sub (intersection t) x by apply: setI_s1.
move=> z oz pz.
have aux: inc z t -> sub y z by move=> zt w wi; apply: (setI_hi wi zt).
case: (ordinal_trichotomy bx oz) => ty.
- by apply: (sub_trans sxt); apply: (ordinal_transitive oz).
- by apply: aux; apply: Zo_i => //;apply/setU1_P; left.
- apply: aux; ue.
Qed.

On an ordinal, inc and sub induce the same ordering, which is a well-ordering

Lemma ordinal_same_wo x: ordinalp x ->
  ordinal_oa x = ordinal_o x.
Proof.
move=> ox.
set_extens t; move/Zo_P => [pa pb]; move/setX_P: (pa) => [_ qa qb];
  move:(ordinal_hi ox qa) (ordinal_hi ox qb) => ra rb; apply/Zo_i => //.
   apply: ordinal_sub3 => //; by apply/setU1_P.
by apply/setU1_P; apply /ordinal_sub4P.
Qed.

Lemma ordinal_o_wor x: ordinalp x -> worder (ordinal_o x).
Proof.
move=> ox.
move: (sub_osr x) => [pa pb].
rewrite /ordinal_o; split => //; rewrite pb.
move=> y yE nex.
have p1: (ordinal_set y) by move=> a ax; move: (yE _ ax) => aE; ord_tac0.
have hh: sub y (substrate (sub_order x)) by ue.
have ix:= (ordinal_setI nex p1).
rewrite /least; aw;ex_tac.
move=> z zy; apply/iorder_gleP => //.
by apply/ordo_leP;split; [apply: yE | apply: yE | apply: setI_s1 ].
Qed.

Lemma ordinal_worder x: ordinalp x ->
  worder (ordinal_oa x).
Proof. by move=> ox; rewrite ordinal_same_wo //; apply: ordinal_o_wor. Qed.

If x is an element of an ordinal E, the set of elements less than x (for the ordering of E) is x

Lemma ordinal_segment1 E x: trans_dec_set E ->
  inc x E -> segment (ordinal_oa E) x = x.
Proof.
move => [tE dE] xE.
suff: segment (ordinal_oa E) x = x \cap E.
  by move => ->; apply/setI2id_Pl; apply: tE.
rewrite /segment /ordinal_oa /interval_uo graph_on_sr //; last by fprops.
set_extens y.
  by move/Zo_hi => [ /graph_on_P1 [pa pb pc] pd]; apply: setI2_i => //;case: pc.
move /setI2_P=> [yx yE]; apply:Zo_i => //;split.
  by apply/graph_on_P1; split => //; left.
move=> xy; rewrite xy in yx; case: (dE _ xE yx).
Qed.

Lemma ordinal_segment E x: ordinalp E ->
  inc x E -> segment (ordinal_o E) x = x.
Proof.
move=> ox xE;rewrite -ordinal_same_wo //.
apply: ordinal_segment1 => //; apply: ordinal_trans_dec =>//.
Qed.

Alternate definition of an ordinal : transitive, asymmetric and inc is a well-ordering

Lemma ordinal_pr1 E:
  ordinalp E <->
  [/\ transitive_set E, worder (ordinal_oa E) & asymmetric_set E].
Proof.
split.
  move=> h; split => //.
  - 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 by move=> u uE uu; case: (aE _ _ uE uE uu uu).
have p0:forall b, inc b E -> inc b b \/ b = b by move=> b bE; right.
have sg: (substrate (ordinal_oa E)) = E by rewrite /ordinal_oa graph_on_sr.
have si: segmentp (ordinal_oa E) X.
  rewrite /segmentp /interval_uo /ordinal_oa sg; split => //.
  move=> x y xX /graph_on_P1 [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 ->]; rewrite ordinal_segment1 //.
Qed.

Lemma ordinal_o_sr E: substrate (ordinal_o E) = E.
Proof. exact: (proj2(sub_osr _)). Qed.

Lemma ordinal_o_or x: order (ordinal_o x).
Proof. exact (proj1 (sub_osr x)). Qed.

Lemma ordinal_o_tor x: ordinalp x -> total_order (ordinal_o x).
Proof. by move=> or; apply: (worder_total (ordinal_o_wor or)). Qed.

Hint Resolve ordinal_o_or ordinal_o_wor: fprops.

Two isomorphic ordinals are equal

Lemma ordinal_isomorphism_unique x y f:
  ordinalp x -> ordinalp y ->
  order_isomorphism f (ordinal_o x)(ordinal_o y) ->
  (x = y /\ f = identity x).
Proof.
move=> ox oy oif.
move: (oif) => [_ _ [[[ff injf] [_ surf]] srcf trgf] pf].
move: srcf trgf; rewrite !ordinal_o_sr // => srcf trgf.
have Wt: forall a, inc a x -> inc (Vf f a) y.
  by move=> a; rewrite - srcf -trgf => asf; Wtac.
have prf2:forall a b, inc a x -> inc b x -> (inc a b <-> inc (Vf f a) (Vf f b)).
  move=> a b ax bx.
  apply: (iff_trans (iff_sym (ordo_ltP ox ax bx))).
  rewrite -! srcf in ax bx.
  apply: (iff_trans (order_isomorphism_siso oif ax bx)).
  apply /ordo_ltP => //; apply/Wt; ue.
rewrite trgf srcf in surf.
case: (p_or_not_p (exists2 z, inc z x & Vf f z <> z)) => H; last first.
  have fi: forall a, inc a x -> Vf f a = a.
  move=> a ax; ex_middle em; case H; ex_tac.
  have xy: x = y.
    set_extens t => tx; first by rewrite - (fi _ tx) - trgf; Wtac.
    by move: (surf _ tx)=> [z zx <-];rewrite (fi _ zx).
  split => //; apply: function_exten;aw; fprops.
    by rewrite xy.
  by move=> a; rewrite srcf;move=> ax; rewrite identity_V //; apply: fi.
move:H => [z0 z0x fz0].
pose p z := inc z x /\ Vf f z <> z.
move: (least_ordinal1 (p:=p) (ordinal_hi ox z0x) (conj z0x fz0)).
set z := (least_ordinal p z0).
move => [oz [zx pb] pc].
have p1: forall a, inc a z -> Vf f a = a.
  move=> a az; ex_middle aux.
  have ax:= (ordinal_transitive ox zx az).
  move: ((pc a (ordinal_hi ox ax) (conj ax aux)) _ az).
  by move: (ordinal_decent ox ax).
case: (ordinal_trichotomy (ordinal_hi oy (Wt _ zx)) oz).
+ rewrite srcf in injf; move => h.
  by move: (injf _ _ (ordinal_transitive ox zx h) zx (p1 _ h)).
+ move => ww.
  have fzy: inc (Vf f z) y by rewrite - trgf; Wtac.
  move:(surf _ (ordinal_transitive oy fzy ww)) => [a ax za].
  rewrite - {1} za in ww.
  by move /(prf2 _ _ ax zx): (ww) => /p1 h2; case pb; rewrite - za h2.
+ done.
Qed.

Any well-ordered set is isomorphic to an ordinal

Lemma ordinal_isomorphism_exists r (f := ordinal_iso r):
  worder r ->
  ordinalp (target f) /\ order_isomorphism f r (ordinal_o (target f)).
Proof.
move=> wor;move: (wor)=> [or worp].
move: (transfinite_defined_pr target wor) => [suf sf vf].
set E:= substrate r.
have fa: function f by fct_tac.
have vf1: forall a b, inc a E ->
  (inc b (Vf f a) <-> (exists2 u, glt r u a & Vf f u = b)).
  move=> a b aE; rewrite (vf _ aE) /restriction_to_segment /restriction1; aw.
  have ssf: sub (segment r a) (source f) by rewrite sf;apply: sub_segment.
  split.
    by move/(Vf_image_P fa ssf) => [x /segmentP pa pb]; exists x.
  move => [x ua ub]; apply/(Vf_image_P fa ssf).
  by exists x => //; apply /segmentP.
have incf3: forall a b, inc a (source f) -> inc b (source f) ->
     sub (Vf f a) (Vf f b) -> 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 (Vf f a) (Vf f a))).
  case: (emptyset_dichot Bad)=> h.
     empty_tac1 b; apply /Zo_i => //.
     by apply: sab; rewrite (vf1 _ _ aE); exists b.
  have BE: (sub Bad E) by rewrite /Bad; apply: Zo_S.
  move: (worp _ BE h) => [y []];aw; move=> /Zo_P [yE iWWy] yp.
  move: (iWWy); rewrite (vf1 _ _ yE); move=> [u us Wu].
  have badu: inc u Bad by apply: Zo_i=>//; [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 (Vf f x) (Vf f y) by rewrite Wxy; fprops.
  have p2: sub (Vf f y) (Vf f x) 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 (Vf f a) (Vf f b)).
  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 => //; order_tac.
have oi: (order_isomorphism f r (ordinal_o (target f))).
  split => //; [fprops | rewrite ordinal_o_sr | move=> x y xsf ysf].
     split => //.
  split; first by move => pa; apply/ordo_leP;split => //; try Wtac; apply: incf.
  move/ordo_leP => [_ _ xy]; apply: (incf3 _ _ xsf ysf xy).
split=>//; apply: ordinal_pr.
  move=> x xt y.
  move: ((proj2 suf) _ xt)=> [z zs <-].
  rewrite sf in zs; rewrite (vf1 _ _ zs).
  move=> [u us <-];Wtac.
  rewrite sf; order_tac.
move=> y ytf; move: ((proj2 suf) _ ytf)=> [z zs <-].
set (Bad:= Zo E (fun z => (~ (ordinalp (Vf f z))))).
case: (emptyset_dichot Bad)=> h.
  by ex_middle h'; empty_tac1 z; apply: Zo_i =>//; rewrite/E - sf.
have sBE:sub Bad E by rewrite /Bad; apply: Zo_S.
move: (worp _ sBE h) => [x []]; aw; move => /Zo_P [xE ioWx] xp.
case: 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 <-].
ex_middle h'.
have ub:inc u Bad by apply: Zo_i => //; rewrite /E;order_tac.
move: (iorder_gle1 (xp _ ub)) => yu; order_tac.
Qed.

ordinal r is the unique ordinal isomorphic to r

Definition ordinal r := target (ordinal_iso r).

Lemma OS_ordinal r: worder r -> ordinalp (ordinal r).
Proof.
by move=> wor; move:(ordinal_isomorphism_exists wor) => [h _].
Qed.

Lemma ordinal_o_is r: worder r -> r \Is (ordinal_o (ordinal r)).
Proof.
move=> wor; move:(ordinal_isomorphism_exists wor) => [_ h].
by exists (ordinal_iso r).
Qed.

Lemma ordinal_o_o E: ordinalp E -> ordinal (ordinal_o E) = E.
Proof.
move=> oE; move: (ordinal_o_wor oE)=> woi.
move: (ordinal_isomorphism_exists woi) => [_ ] h.
by move: (ordinal_isomorphism_unique oE (OS_ordinal woi) h) => [res _].
Qed.

Lemma ordinal_o_isu x y:
  ordinalp x -> ordinalp y ->
  (ordinal_o x) \Is (ordinal_o y) -> x = y.
Proof.
by move=> ox oy [f fi]; move: (ordinal_isomorphism_unique ox oy fi) => [].
Qed.

Lemma ordinal_o_isu1 r r': worder r -> worder r' ->
  r \Is r' -> ordinal r = ordinal r'.
Proof.
move=> w1 w2 or.
move: (OS_ordinal w1)(OS_ordinal w2) => o1 o2.
move: (ordinal_o_is w1)(ordinal_o_is w2) => i1 i2.
apply: (ordinal_o_isu o1 o2 (orderIT (orderIT (orderIS i1) or) i2)).
Qed.

Lemma ordinal_o_isu2 r E: worder r -> ordinalp E ->
  r \Is (ordinal_o E) -> ordinal r = E.
Proof.
move=> wo bo oi.
by rewrite (ordinal_o_isu1 wo (ordinal_o_wor bo) oi) (ordinal_o_o bo).
Qed.

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

Definition the_ordinal_iso r := (inverse_fun (ordinal_iso r )).

Lemma the_ordinal_iso1 r : worder r ->
  order_isomorphism (the_ordinal_iso r) (ordinal_o (ordinal r)) r.
Proof.
move=> wor; exact(inverse_order_is (proj2 (ordinal_isomorphism_exists wor))).
Qed.

Lemma the_ordinal_iso2 r g:
  worder r -> order_isomorphism g (ordinal_o (ordinal r)) r ->
  g = the_ordinal_iso r.
Proof.
move =>wor; move: (the_ordinal_iso1 wor) => is1 is2.
move: (OS_ordinal wor) => ox.
move: (ordinal_o_wor ox) => wor2.
move: (order_isomorphism_w is1) => m1.
move: (order_isomorphism_w is2) => m2.
have pc: segmentp r (substrate r) by apply: substrate_segment; fprops.
have pa: segmentp r (range (graph (the_ordinal_iso r))).
  move: is1 => [_ _ [[_ sf] _ tf] _].
  by rewrite (surjective_pr3 sf) tf.
have pb: segmentp r (range (graph g)).
  move: is2 => [_ _ [[_ sf] _ tf] _].
  by rewrite (surjective_pr3 sf) tf.
exact (isomorphism_worder_unique wor2 wor pb pa m2 m1).
Qed.

We can compare two orderings; this is compatible with order isomorphism. If E and E' are two ordinals ordered by r and r', then ordinal_leD1 E E' says r <= r'. In this case we have r <= r' iff r is isomorphic to a segment of r'. We have r < r' iff r is isomorphic to segment r' x for some x.

Definition order_le r r' :=
  [/\ order r, order r' &
  exists f x,
      sub x (substrate r') /\ order_isomorphism f r (induced_order r' x)].

Lemma order_le_compatible r r' r1 r1':
  r \Is r1 -> r' \Is r1' ->
  (order_le r r' <-> order_le r1 r1').
Proof.
move: r r' r1 r1'.
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; split;apply: aux=>//; apply: orderIS.
move => r1 r2 r3 r4 /orderIS [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]]]]].
split => //.
set Y:= image_by_fun g X.
have sY: sub Y (substrate r4) by rewrite -tg; apply:fun_image_Starget1; fct_tac.
have fg: function g by fct_tac.
have ff: function f by fct_tac.
have fh: function h by fct_tac.
have sX': sub X (source g) by ue.
have Yp1: forall x, inc x X -> inc (Vf g x) Y.
  move=> x xX; apply /(Vf_image_P fg sX'); ex_tac.
have Yp2: forall y, inc y Y -> exists2 x, inc x X & y = Vf g x.
   by move=> y; move/(Vf_image_P fg sX').
move: th; aw => th.
pose k x := Vf g (Vf h (Vf f x)).
have ta1: forall x, inc x (substrate r3) -> inc (k x) Y.
  rewrite - sf /k; move=> t ts; apply: Yp1.
  move: (Vf_target ff ts); rewrite tf - sh => Wt; rewrite -th; Wtac.
exists (Lf k (substrate r3) Y); exists Y; split => //.
have aux: bijection (Lf k (substrate r3) Y).
  apply: lf_bijective => //.
    rewrite - sf; move=> u v us vs eq.
    move: (Vf_target ff us) (Vf_target ff vs) => Wt1 Wt2.
    rewrite tf - sh in Wt1 Wt2.
    move: (Vf_target fh Wt1)(Vf_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: ((proj2 srh) _ xX)=> [v vsf <-].
  rewrite sh - tf in vsf.
  move: ((proj2 srf) _ vsf)=> [w wsc <-].
  rewrite - sf; ex_tac.
move: (iorder_osr o4 sY) => [or4 sr4].
split => //.
  by rewrite sr4 /bijection_prop; aw.
red; aw; move=> u v us vs; aw.
rewrite - sf in us vs; apply: (iff_trans (oif _ _ us vs)).
move: (Vf_target ff us) (Vf_target ff vs); rewrite tf - sh => Wt1 Wt2.
move: (Vf_target fh Wt1)(Vf_target fh Wt2); rewrite th =>Vt1 Vt2.
move: (sX' _ Vt1) (sX' _ Vt2) => U1 U2; move: (Yp1 _ Vt1)(Yp1 _ Vt2) => X1 X2.
apply: (iff_trans (oih _ _ Wt1 Wt2)).
apply: (iff_trans(iorder_gleP r2 Vt1 Vt2)).
apply: (iff_trans (oig _ _ U1 U2)); symmetry; exact: iorder_gleP.
Qed.

We say r <= r' if there is a order morphism; this is the same as saying that there is an isomorphism onto a subset of r'

Lemma order_le_alt r r':
  order r -> order r' -> (exists f, order_morphism f r r') ->
  order_le r r'.
Proof.
move => or or' [f om]; split => //.
move: om (order_morphism_fi om) => [oa oc [ff sf tf] isof] injf.
move: (restriction_to_imageE ff); set g := restriction_to_image f => eq.
have Xs: sub (target g) (substrate r').
  by move => t; rewrite - tf eq/restriction1; aw; apply:fun_image_Starget.
move:(iorder_osr or' Xs)=> [or1 sr1].
have bg:bijection g by apply:restriction_to_image_fb.
have ss: source f = source g by rewrite eq /restriction1; aw.
have aux: forall x, inc x (source g) -> Vf g x = Vf f x.
  move => x xsf; rewrite eq restriction1_V //; ue.
exists g, (target g); split => //; split => //; first by split => //; ue.
move => x y xsg ysg.
apply: (iff_trans (_: gle r x y <-> (gle r' (Vf g x) (Vf g y)))).
  by rewrite (aux _ xsg) (aux _ ysg); apply: isof; rewrite ss.
split => pa; first by apply/iorder_gleP => //; Wtac; apply: bij_function.
exact: (iorder_gle1 pa).
Qed.

Lemma order_le_alt2 f r r' x: order r -> order r' ->
  sub x (substrate r') ->
  let F := (Lf (Vf f) (substrate r) (substrate r')) in
    order_isomorphism f r (induced_order r' x)
    -> (order_morphism F r r' /\ range (graph F) = x).
Proof.
move=> oa ob sxa F [ou ov' [iz sz tz] siz].
rewrite iorder_sr // in tz.
have fh: function f by fct_tac.
have ta1: lf_axiom (Vf f) (substrate r) (substrate r').
  move=> t tu; apply: sxa; Wtac.
have fF: function F by apply: lf_function.
have rg: range (graph F) = x.
  have gF:sgraph (graph F) by fprops.
  rewrite - tz ;set_extens w.
    move/(rangeP gF) => [x0 Jg].
    move: (p1graph_source fF Jg); rewrite /F; aw => xx.
    rewrite (Vf_pr fF Jg); rewrite /F;aw; Wtac.
  move=> wt;move: iz =>[_ sjh]; move: ((proj2 sjh) _ wt) => [x0 xs <-].
  apply/(rangeP gF); exists x0.
  have ->: Vf f x0 = Vf F x0 by rewrite /F; aw; ue.
  apply: Vf_pr3 =>//; rewrite /F; aw; ue.
split =>//;rewrite /F; split => //; first by red; aw.
red; aw => x1 x2 x1s x2s; aw.
rewrite - sz in x1s x2s; apply: (iff_trans (siz _ _ x1s x2s)).
split; first by move/iorder_gle1.
move => hh; apply/iorder_gleP => //; rewrite - tz; Wtac.
Qed.

Definition ordinal_leD1 r r' :=
  [/\ ordinalp r, ordinalp r' & order_le (ordinal_o r)(ordinal_o r')].

Lemma order_le_compatible1 r r':
  worder r -> worder r' ->
  (order_le r r' <-> ordinal_leD1 (ordinal r) (ordinal r')).
Proof.
move=> wo1 wo2.
move: (ordinal_o_is wo1)(ordinal_o_is wo2) => oi1 oi2.
move: (OS_ordinal wo1)(OS_ordinal wo2) => o1 o2.
rewrite (order_le_compatible oi1 oi2); rewrite /ordinal_leD1.
by split => //; move => [_ _].
Qed.

Lemma ordinal_le_P x x':
   ordinal_leD1 x x' <->
   [/\ ordinalp x, ordinalp x' &
     exists f S,
      segmentp (ordinal_o x') S /\
      order_isomorphism f (ordinal_o x) (induced_order (ordinal_o x') S)].
Proof.
split.
  move=> [or or' [otr otr' [f [t [sx iso]]]]];split => //.
  move:(isomorphic_subset_segment (ordinal_o_wor or') sx) => [w [g [sw isg]]].
  exists (g \co f); exists w; split => //.
  apply: (compose_order_is iso isg).
move=> [or or' [f [t [[sx sxp] oi]]]];split => //; split; fprops.
by exists f, t.
Qed.

Lemma ordinal_le_P1 x x':
   ordinal_leD1 x x' <->
   [/\ ordinalp x, ordinalp x' &
     exists2 f, segmentp (ordinal_o x') (range (graph f)) &
         order_morphism f (ordinal_o x)(ordinal_o x')].
Proof.
split; last first.
  move=> [or or'[f _ mf]]; split => //.
  move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _].
  by apply / (order_le_alt o1 o2); exists f.
move /ordinal_le_P; move => [or or' [f [t [sx isof]]]]; split => //.
move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _].
have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment1.
move: (order_le_alt2 o1 o2 sxs isof).
set g := Lf _ _ _.
by move => [om xp]; exists g; rewrite ? xp.
Qed.

Lemma ordinal_lt_P1 x x':
   (ordinal_leD1 x x' /\ x <> x') <->
   [/\ ordinalp x, ordinalp x' &
     exists f y,
        [/\ inc y x',
        (range (graph f)) = segment (ordinal_o x') y
        & order_morphism f (ordinal_o x) (ordinal_o x')]].
Proof.
split.
  move => [] /ordinal_le_P1 [or or' [f srf om]] nrr'.
  case: (well_ordered_segment (ordinal_o_wor or') srf).
  move=> v; case: nrr'; apply: ordinal_o_isu => //.
  move: (order_morphism_fi om) => injf.
  move: om => [o1 o2 [ff sf tf] mf].
  exists f; split => //; split => //.
    split => //;apply: surjective_pr4; [fct_tac |rewrite tf v //].
  move=> [t xsr rgf].
  split => //; exists f; exists t; split => //.
  by rewrite - (ordinal_o_sr x').
move=> [or or' [f [t [xsr rgf om]]]].
move: (ordinal_o_wor or') => wodr.
move: (wodr)=> [odr _].
have p1: segmentp (ordinal_o x') (range (graph f)).
  by rewrite rgf;apply: segment_segment =>//; rewrite ordinal_o_sr //.
  split; first by apply /ordinal_le_P1 => //; split => //;exists f.
move=> rr'; rewrite rr' in om.
move: (unique_isomorphism_onto_segment wodr p1 om); rewrite ordinal_o_sr => idf.
have xrg: inc t (segment (ordinal_o x') t).
   by rewrite - rgf idf /identity; aw; rewrite identity_r.
apply: (not_in_segment xrg).
Qed.

Lemma ordinal_lt_P x x':
  (ordinal_leD1 x x' /\ x <> x') <->
   [/\ ordinalp x, ordinalp x' &
     exists f y',
        inc y' x' /\
      order_isomorphism f (ordinal_o x)
       (induced_order (ordinal_o x') (segment (ordinal_o x') y') )].
Proof.
split; last first.
  move => [or or' [f [y [sx isof]]]]; apply /ordinal_lt_P1; split => //.
  move:(ordinal_o_wor or) (ordinal_o_wor or')=> [o1 _][o2 _].
  set t := segment (ordinal_o x') y.
  have sxs: sub t (substrate (ordinal_o x')) by apply: sub_segment.
  move: (order_le_alt2 o1 o2 sxs isof).
  by set g := Lf _ _ _; move => [om xp]; exists g, y.
move /ordinal_lt_P1.
set r := (ordinal_o x); set r':= (ordinal_o x').
move=> [or or' [f [y [pa pb pc]]]]; split => //.
move: pc (order_morphism_fi pc) => [oa oc [ff sf tf] isof] injf.
move: (restriction_to_imageE ff) => eq.
set g := restriction_to_image f.
have tg : target g = segment r' y.
  rewrite /g eq /restriction1; aw; rewrite - pb - image_by_fun_source //.
have Xs: sub (target g) (substrate r') by rewrite tg; apply: sub_segment.
move:(iorder_osr oc Xs)=> [or1 sr1].
have bg:bijection g by apply:restriction_to_image_fb.
have ss: source f = source g by rewrite /g eq /restriction1; aw.
have aux: forall x, inc x (source g) -> Vf g x = Vf f x.
    move => t xsf; rewrite /g eq restriction1_V //; ue.
exists g, y; rewrite - tg;split => //; split => //;first by split => //; ue.
move => u v xsg ysg.
apply: (iff_trans (_: gle r u v <-> (gle r' (Vf g u) (Vf g v)))).
  by rewrite (aux _ xsg) (aux _ ysg); apply: isof; rewrite ss.
split => pd; first by apply/iorder_gleP => //; Wtac; apply: bij_function.
exact: (iorder_gle1 pd).
Qed.

Lemma ordinal_lt_pr2 a b:
  worder b -> (ordinal_leD1 a (ordinal b) /\ a <> (ordinal b)) ->
     exists f x,
       [/\ inc x (substrate b),
        (range (graph f)) = segment b x & order_morphism f (ordinal_o a) b].
Proof.
move=> ob ltab; move: (ltab) =>[[oa _] _]; move: ltab.
move /ordinal_lt_P1; move=> [_ op [f [x [xsp rgx om]]]].
have [g oig]: order_isomorphic (ordinal_o (ordinal b)) b.
  by apply: orderIS; apply: (ordinal_o_is ob).
move: om (oig) => [o1 o2 [ff sf tf] pf][_ o4 [[gi gs] sg tg] pg].
have cfg: composable g f by split => //; try fct_tac; ue.
rewrite ! ordinal_o_sr // in tf sf sg.
have p0: function (g \co f) by fct_tac.
have p3: order_morphism (g \co f) (ordinal_o a) b.
  split=> //; first by split;aw; rewrite ordinal_o_sr.
  red; aw; move=> u v asf bsf; aw.
  apply: (iff_trans (pf _ _ asf bsf)); apply/ pg; rewrite sg - tf; Wtac.
set y:= (Vf g x).
have p1: inc y (substrate b) by rewrite /y;Wtac; fct_tac.
exists (g \co f); exists y; split => //.
set_extens u.
  move /(range_fP p0)=> [v vsf uvW].
  move: vsf; aw => vsf.
  have: inc (Vf f v) (segment (ordinal_o (ordinal b)) x).
     rewrite -rgx; Wtac.
  move /segmentP => xx; apply /segmentP; rewrite /y uvW; aw.
  by apply (order_isomorphism_sincr oig).
move/segmentP=> buy.
have utg: inc u (target g) by rewrite tg; order_tac.
move: ((proj2 gs) _ utg) buy => [v vsg Wvg].
rewrite - sg in xsp.
rewrite /y -Wvg; move/(order_isomorphism_siso oig vsg xsp) => /segmentP.
rewrite -rgx; move/(range_fP ff) => [w pa pb].
apply/(range_fP p0); aw; ex_tac; rewrite pb; aw.
Qed.

Lemma ordinal_le_P0 x y:
  ordinal_leD1 x y <-> [/\ ordinalp x, ordinalp y & sub x y].
Proof.
split; last first.
  rewrite /ordinal_leD1; move => [ox oy sxy];split => //.
  move: (ordinal_o_wor ox) => wox.
  move: (wox) => [orx _].
  red; rewrite ordinal_o_sr //; split; fprops.
  exists (identity x); exists x; split => //.
  have ->: induced_order (ordinal_o y) x = (ordinal_o x).
     rewrite /ordinal_o/induced_order/ordinal_o/graph_on.
     set_extens t.
       by move => /setI2_P [] /Zo_P [pa pb] pc; apply: Zo_i.
     move =>/ Zo_P [pa pb]; apply/setI2_P;split => //; apply: Zo_i => //.
     by apply: (setX_Slr sxy sxy).
  rewrite - {1} (ordinal_o_sr x) ; by apply: identity_is.
move /ordinal_le_P => [ox oy [f [S [sS oi]]]]; split => //.
move: (ordinal_o_wor oy) => woy.
have [p1 p2 p3]:
   [/\ sub S y, ordinalp 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_o_sr =>//.
    move => ->; split => //; rewrite iorder_substrate //.
    by move: woy => [ok _].
  move=> [u]; rewrite ordinal_o_sr =>// uy.
  rewrite ordinal_segment //.
  move: (ordinal_transitive oy uy) => suy.
  move=> ->; split => //; first by ord_tac0.
  set_extens t; first by move/setI2_P => [] /Zo_P [pa pb] pc;apply /Zo_P; split.
  move/Zo_P =>[pa pb]; apply/setI2_i => //.
  by apply: Zo_i => //;apply:(setX_Sll suy).
rewrite p3 in oi.
by move: (ordinal_isomorphism_unique ox p2 oi)=>[-> _].
Qed.

ordinal_leD1 E E' simplifies to sub E E' when E and E' are ordinals

Definition ordinal_le x y :=
  [/\ ordinalp x, ordinalp y & sub x y].
Definition ordinal_lt x y := ordinal_le x y /\ x <> y.

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

Lemma ord_leP a: ordinalp a ->
  forall x, (x <=o a <-> inc x (succ_o a)).
Proof.
move=> oa x; split.
 by move=> [pa pb pc]; apply /ordinal_sub4P.
move=> aux; move: (ordinal_sub3 oa aux) => xa; split => //.
apply: (ordinal_hi (OS_succ oa) aux).
Qed.

We study here ordinal_le; it is a well-ordering

Lemma ord_ltP0 x y:
  x <o y <-> [/\ ordinalp x, ordinalp y & inc x y].
Proof.
split.
   move=> [[ox oy sxy] nxy]; split => //; case: (ordinal_sub ox oy sxy) => //.
by move=> [ox oy xy]; move: (ordinal_sub2 oy xy) => [pa pb].
Qed.

Lemma ord_ltP a: ordinalp a -> forall x, (x <o a <-> inc x a).
Proof.
move=> oa x; split; first by move/ord_ltP0 => [_].
move => xa; apply/ord_ltP0; split => //; ord_tac0.
Qed.

Theorem wordering_ordinal_le: worder_r ordinal_le.
Proof.
split; first split.
  - move=> x y z [Kx Ky xy][_ Kz yz].
    split => //; by apply: sub_trans yz.
  - move=> x y [Kx Ky xy][_ _ yx].
    by apply: extensionality.
  - by move=> x y [ox oy _]; split => //;split => //.
move=> x ale nex.
have alo: ordinal_set x by move=> a /ale [h _].
set y := (intersection x).
have yx:inc y x by apply: ordinal_setI.
exists y.
red; rewrite (graph_on_sr ale); split=> // a ax.
move: (alo _ ax) (alo _ yx) => Ka Ky.
by apply /graph_on_P1;split => //; split => //; apply: setI_s1.
Qed.

Lemma wordering_ordinal_le_pr x:
  ordinal_set x -> worder_on (graph_on ordinal_le x) x.
Proof.
move => osx.
apply: wordering_pr; first by apply: wordering_ordinal_le.
by move => a /osx ox; split.
Qed.

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

Lemma order_leR x: order x -> order_le x x.
Proof.
move=> ox; split => //; exists (identity (substrate x)); exists (substrate x).
have ss: sub (substrate x) (substrate x) by [].
move: (iorder_osr ox ss) => [pa pb].
split => //;hnf;rewrite /bijection_prop identity_s identity_t pb.
split => //; first by split => //;apply: identity_fb.
red; aw; move=> z y xsr ysr; bw.
symmetry; exact:(iorder_gleP x xsr ysr).
Qed.

Lemma ord_leR x: ordinalp x -> x <=o x.
Proof. move=> or; split => //. Qed.

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

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

Lemma ord_leA1 a b: a <=o b -> b <o a -> False.
Proof. by move=> ole [olt one]; case: one; apply: ord_leA. Qed.

Lemma ord_lt_leT a b c: a <o b -> b <=o c -> a <o c.
Proof.
move=> [ab nab] bc; split; first by apply: (ord_leT ab bc).
by dneg ac; rewrite -ac in bc; apply: ord_leA.
Qed.

Lemma ord_le_ltT a b c: a <=o b -> b <o c -> a <o c.
Proof.
move=> ab [bc nbc]; split; first by apply: (ord_leT ab bc).
by dneg ca; rewrite ca in ab; apply: ord_leA.
Qed.

Lemma ord_lt_ltT a b c: a <o b -> b <o c -> a <o c.
Proof. by move=> [ab _] bc; apply: (ord_le_ltT ab bc). Qed.

Lemma ord_le_to_el a b:
  ordinalp a -> ordinalp b ->
  a <=o b \/ b <o a.
Proof.
move=> oa ob.
case: (ordinal_trichotomy oa ob).
- move => h; move: (ordinal_sub2 ob h) => [pa pb]; left; split => //.
- by right; apply/ord_ltP0.
- by move=> ->; left; apply:ord_leR.
Qed.

Lemma ord_le_to_ell a b:
 ordinalp a -> ordinalp b ->
 [\/ a = b, a <o b | b <o a].
Proof.
move=> oa ob.
case: (ord_le_to_el oa ob) => h;case: (equal_or_not a b) => ab; in_TP4.
Qed.

Lemma ord_le_to_ee a b:
  ordinalp a -> ordinalp b -> a <=o b \/ b <=o a.
Proof.
by move=> oa ob; case: (ord_le_to_el oa ob); [by left | move => [h _]; right ].
Qed.

Lemma ord_le_to_si a b:
  ordinalp a -> ordinalp b -> (sub a b \/ inc b a).
Proof.
move=> oa ob; case: (ord_le_to_el oa ob); first by move => [_ _]; left.
by move/ord_ltP0 => [_ _]; right.
Qed.

Ltac ord_tac :=
  match goal with
    | h: _ <=o ?x |- ordinalp ?x
      => move: h => [_ h _]; exact h
    | h: ?x <=o _ |- ordinalp ?x
      => move: h => [h _ _]; exact h
    | h: _ <o ?x |- ordinalp ?x
      => move: h => [[_ h _] _]; exact h
    | h: ?x <o _ |- ordinalp ?x
      => move: h => [[h _ _] _]; exact h
    | h1: ?x <=o ?y, h2: ?y <=o ?x |- ?x = ?y
      => apply: (ord_leA h1 h2)
    | h1: ?x <=o ?y, h2: ?y <=o ?z |- ?x <=o ?z
      => apply: (ord_leT h1 h2)
    | h1: ?x <o ?y, h2: ?y <=o ?z |- ?x <o ?z
      => apply: (ord_lt_leT h1 h2)
    | h1: ?x <=o ?y, h2: ?y <o ?z |- ?x <o ?z
      => apply: (ord_le_ltT h1 h2)
    | h1: ?x <o ?y, h2: ?y <o ?z |- ?x <o ?z
      => apply: (ord_lt_ltT h1 h2)
    | h1: ?x <=o ?y, h2: ?y <o ?x |- _
      => case: (ord_leA1 h1 h2)
    | h1: ordinalp ?x, h2: inc ?y ?x |- ordinalp ?y
      => apply: (ordinal_hi h1 h2)
    | h1: ordinalp ?x |- ?x <=o ?x
      => apply: (ord_leR h1)
    | h1: ?x <o ?y |- ?x <=o ?y
      => by move: h1 => []
  | h1: ordinalp ?a, h2: inc ?x ?a |- ?x <o ?a =>
     by apply/(ord_ltP h1)
  | h2: ?x <o ?a |- inc ?x ?a =>
     by move/ord_ltP0: h2 => [_ _]
  | h1: ordinalp ?a, h2: inc ?x ?a |- ?x <=o ?a =>
     by move: h2 => /(ord_ltP h1) []
  | h1: ?x = succ_o ?y |- inc ?y ?x => by rewrite h1; fprops
end.

Lemma order_cp0 r r': order r -> order r' ->
  ((sub r r') <-> (forall x y, gle r x y -> gle r' x y)).
Proof.
move => or or'; split; first by move => h x y xy; apply: h.
move => h t tr.
move: (or) => [gr _ _ _]; move: (gr _ tr) => p; rewrite -p.
by apply: h; hnf; rewrite p.
Qed.

Lemma order_cp1 x y: worder x -> worder y -> sub x y ->
  (sub (substrate x) (substrate y) /\ x = (induced_order y (substrate x))).
Proof.
move => wo1 wo2 xy.
move: (wo1) (wo2) => [o1 _] [o2 _].
have aa: sub (substrate x) (substrate y).
  move => t tsa; apply /(order_reflexivityP o2); apply: xy.
  by apply /(order_reflexivityP o1).
move: (iorder_osr o2 aa) => [sa sb].
split => //; apply: extensionality.
   move => t tx; apply /setI2_P; split; fprops.
   apply:sub_graph_coarse_substrate; fprops.
move => t /setI2_P [ty /setX_P [pa pb pc]]; rewrite - pa.
case: (proj2 (worder_total wo1) _ _ pb pc) => // h2.
rewrite -pa in ty.
move: (order_antisymmetry o2 (xy _ h2) ty) => h3; by move: h2; rewrite h3.
Qed.

Lemma order_cp2 x y: worder x -> worder y -> sub x y -> ordinal x <=o ordinal y.
Proof.
move => wo1 wo2 xy.
move: (order_cp1 wo1 wo2 xy) => [pa pb].
suff: order_le x y by move /(order_le_compatible1 wo1 wo2) /ordinal_le_P0.
split; fprops; exists (identity (substrate x)), (substrate x); split => //.
rewrite -pb; apply: identity_is; fprops.
Qed.

Lemma order_cp3 x y: worder x -> worder y ->
   ssub x y -> (segmentp y (substrate x)) -> ordinal x <o ordinal y.
Proof.
move => wo1 wo2 [xy xny] sp.
split; first by apply: order_cp2.
move => so.
move: (ordinal_o_is wo2) (orderIS (ordinal_o_is wo1)); rewrite so => pa pb.
move: (order_cp1 wo1 wo2 xy) => [ss xx].
move: (orderIT pa pb) => [f [sa sb [sc sd se] sf]].
have ff: function f by apply: bij_function.
set g := Lf (fun z => Vf f z) (substrate y) (substrate y).
have ta: lf_axiom (fun z => Vf f z) (substrate y) (substrate y).
  by move => t ty; apply: ss; rewrite - se; Wtac.
have fg: function g by apply: lf_function.
have sfsg: source f = source g by rewrite /g; aw.
have gv: forall t, inc t (source g) -> Vf g t = Vf f t.
  rewrite /g; aw => t tf; aw.
have rg: range (graph g) = substrate x.
  set_extens t; first by move/(range_fP fg) => [a ag ->];rewrite gv//; Wtac; ue.
  rewrite - se; move/ (proj2 (proj2 sc))=> [z]; rewrite sfsg => zg.
  move => <-; rewrite - (gv _ zg); apply/(range_fP fg); ex_tac.
have pd: segmentp y (range (graph g)) by rewrite rg.
have pc: order_morphism g y y.
  split => //; first by rewrite /g; split;aw.
  move => u v ug vg; rewrite (gv _ ug) (gv _ vg).
  rewrite - sfsg in ug vg; split; first by move/(sf u v ug vg); apply: xy.
  move => le1; move:(sf v u vg ug) => aux.
  move: (proj2 (proj1 sc) _ _ ug vg) => injf.
  rewrite sd in ug vg;case: (proj2 (worder_total wo2) _ _ ug vg) => // le2.
  have le3:gle y (Vf f v) (Vf f u) by move /aux: le2; apply: xy.
  by move: le2; rewrite (injf (order_antisymmetry (proj1 wo2) le1 le3)).
move: rg; rewrite (unique_isomorphism_onto_segment wo2 pd pc).
rewrite /identity; aw; rewrite identity_r => srr.
by case: xny; rewrite xx - srr (iorder_substrate (proj1 wo2)).
Qed.

We study the properties of the least ordinal

Lemma least_ordinal4 x (p: property) (y := least_ordinal p x):
 ordinalp x -> p x ->
   [/\ ordinalp y, p y & (forall z, ordinalp z -> p z -> y <=o z) ].
Proof.
move=> ox px; move: (least_ordinal1 ox px) => [p1 p2 p3].
split => //; move=> t ot pt;move: (p3 _ ot pt) => zt; red;split => //.
Qed.

Lemma least_ordinal2 (p: property) x:
  (forall y, ordinalp y -> (forall z, z <o y -> p z) -> p y) ->
  ordinalp x -> p x.
Proof.
move => h ox; ex_middle nx.
move: (least_ordinal4 (p:= (fun z => ~ p z)) ox nx) => [p1 p2 p3].
case: p2; apply: h => // z zx.
ex_middle bad; move:(p3 _ (proj31_1 zx) bad) => le; ord_tac.
Qed.

Lemma least_ordinal3 x (p: property) (y := least_ordinal (fun z => (~ p z)) x):
 ordinalp x -> ~ (p x) ->
   [/\ ordinalp y, ~(p y) & (forall z, z <o y -> p z)].
Proof.
move=> ox px.
move: (least_ordinal4 (p:= (fun z => ~ p z)) ox px) => [p1 p2 p3].
split => //; move=> z zy.
have oz: ordinalp z by ord_tac.
ex_middle npz; move: (p3 _ oz npz) => lt; ord_tac.
Qed.

Lemma least_ordinal6 x (p:property) (y :=least_ordinal (fun z => ~ p z) x):
  ordinalp x ->
  p x \/ [/\ ordinalp y, forall z, inc z y -> p z & ~ p y].
Proof.
move => oc; case: (p_or_not_p (p x)) => np; [by left | right].
move:(least_ordinal3 oc np) => [pa pb pc]; split => //.
move => z /(ord_ltP pa); apply: pc.
Qed.

union is the supremum of a family of ordinals, cardinals or the predecessor of an ordinal. We study here the supremum of ordinals

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

Definition ordinal_ub E x:= forall i, inc i E -> i <=o x.

Lemma OS_sup E: ordinal_set E -> ordinalp (\osup E).
Proof.
move=> alo; apply: ordinal_pr.
  apply: transitive_setU =>//.
  by move=> y yx; apply: ordinal_transitive; apply: alo.
move=> y /setU_P [a ya ax].
apply: (ordinal_hi (alo _ ax) ya).
Qed.

Lemma ord_sup_ub E: ordinal_set E -> ordinal_ub E (\osup E).
Proof.
by move=> Ep i iE; split; [ apply: Ep | apply: OS_sup | apply: setU_s1].
Qed.

Lemma ord_ub_sup E y: ordinal_set E ->
  ordinalp y -> ordinal_ub E y ->
  (\osup E) <=o y.
Proof.
move=> /OS_sup Ep oy h; split => //.
by move=> i /setU_P [z iz /h [_ _]]; apply.
Qed.

Lemma ord_sup_prop E: ordinal_set E ->
  exists! x, ordinalp x /\
   (forall y, x <=o y <-> (ordinalp y /\ ordinal_ub E y)).
Proof.
move=> alo; set p := fun x: Set => _; apply /unique_existence;split.
  have ou:= (OS_sup alo).
  exists (\osup E); rewrite /p; split => //; move => y; split.
    move => h.
    have oy: ordinalp y by ord_tac.
    split => //; move=> i iE; exact (ord_leT (ord_sup_ub alo iE) h).
  by move=> [oy aly]; apply: ord_ub_sup.
have p1: forall x, p x -> ordinal_ub E x.
  rewrite /p; move=> t [ox Ex].
  have : t <=o t by ord_tac.
  by rewrite (Ex t); move => [_].
have p2: forall x y, p x -> ordinalp y ->
  (ordinal_ub E y) -> x <=o y.
  rewrite /p; move=> x1 y1 [ox opf] oy h; rewrite opf; split => //.
move=> x y fx fy.
have ox: ordinalp x by move: fx => [ox _ ].
have oy: ordinalp y by move: fy => [oy _ ].
move: (p2 _ _ fy ox (p1 _ fx)) (p2 _ _ fx oy (p1 _ fy))=> h1 h2.
ord_tac.
Qed.

The empty set is the least ordinal

Definition ord_zero := emptyset.
Notation "\0o" := ord_zero.

Lemma OS0: ordinalp \0o.
Proof. move => y ye _ yne; case: yne; apply: extensionality; fprops. Qed.

Lemma ozero_least x: ordinalp x -> \0o <=o x.
Proof. move=> ox; split; fprops; apply: OS0. Qed.

Lemma ord_ne0_pos x: ordinalp x -> x <> \0o -> \0o <o x.
Proof. by move => ox xnz; split; [ apply: ozero_least | apply nesym ]. Qed.

Lemma ord_le0 x: x <=o \0o -> x = \0o.
Proof. move/(ord_leP OS0) => /setU1_P; case => //; case; case. Qed.

Lemma ord_ne_pos x: ordinalp x -> nonempty x -> \0o <o x.
Proof. by move=> ox /nonemptyP nex; apply:ord_ne0_pos. Qed.

Lemma ord_ne_has0 x: ordinalp x -> x <> \0o -> inc \0o x.
Proof.
move=> ox xnz.
by case: (ordinal_sub OS0 ox (sub0_set x)) => // eqz; case: xnz.
Qed.

Lemma ord_lt0 x: x <o \0o -> False.
Proof. by move=> [pa pab]; move: (ord_le0 pa). Qed.

Lemma ord_gt_ne0 x y: x <o y -> y <> \0o.
Proof. move => xy yz; rewrite yz in xy; exact: (ord_lt0 xy). Qed.

succ_o x is the next ordinal after x

Lemma osucc_pr x (z:= succ_o x): ordinalp x ->
  x <o z /\ (forall w, x <o w -> z <=o w).
Proof.
move=> ox; move: (OS_succ ox)=> oy.
split; first by apply/ord_ltP0; split => //; rewrite /z; fprops.
move=> w /ord_ltP0 [_ ow xw].
split => //; move=> t /setU1_P;case; last by move=> ->.
by apply: (ordinal_transitive ow).
Qed.

Lemma ord_succ_lt a: ordinalp a -> a <o (succ_o a).
Proof. move=> oa; apply /ord_ltP0; split;fprops. Qed.

Lemma ord_lt_succP a b: a <o (succ_o b) <-> a <=o b.
Proof.
split.
  move /ord_ltP0=> [p1 /OS_succr p2 p3].
  by split => //; apply: ordinal_sub3.
move => [p1 p2]; move/(ordinal_sub4P p1 p2) => q; apply/ord_ltP0.
split; fprops.
Qed.

Lemma ord_succ_ltP a b: a <o b <-> (succ_o a) <=o b.
Proof.
split.
  by move => h; apply /(proj2 (osucc_pr (proj31_1 h))).
move => [pa pb pc]; have asa:= (pc _ (setU1_1 a a)).
apply /ord_ltP0;split => //; ord_tac.
Qed.

Lemma ord_le_succ_succP x y: x <=o y <-> (succ_o x <=o succ_o y).
Proof.
split => h; first by apply /ord_succ_ltP /ord_lt_succP.
by apply /ord_lt_succP /ord_succ_ltP.
Qed.

Lemma ord_lt_succ_succP x y: (x <o y) <-> (succ_o x <o succ_o y).
Proof.
split => h; first by apply /ord_lt_succP /ord_succ_ltP.
by apply /ord_succ_ltP /ord_lt_succP.
Qed.

Definition succ_op x := exists2 y, ordinalp y & x = succ_o y.

Lemma succ_op_pr a: ordinalp a -> (exists b, a = succ_o b) ->
  exists2 b, ordinalp b & a = succ_o b.
Proof. by move => oa [b bs]; exists b=> //; apply: OS_succr; rewrite - bs. Qed.

Lemma osuccVidpred x: ordinalp x ->
  exactly_one (succ_op x) (x = \opred x).
Proof.
move=> ox.
case: (equal_or_not x (union x)) => h.
  split; [by right | move=> [[y oy yt] _] ].
  have: inc y x by rewrite yt; fprops.
  rewrite h => /setU_P [a ya]; rewrite yt => ay.
  move/(ord_ltP (OS_succ oy)): ay => /ord_lt_succP ay1.
  exact: (ordinal_irreflexive oy (proj33 ay1 _ ya)).
split; [left; apply:succ_op_pr => // | by case].
have p1: sub (union x) x by move=> t /setU_P [y ty yx]; ord_tac0.
move: (setC_ne (conj p1 (nesym h))) => [y /setC_P [yx yp]].
have p3: sub (succ_o y) x.
  move =>t /setU1_P; case; [ move => ty;ord_tac0 | by move=> ->].
have oy:=(OS_succ (ordinal_hi ox yx)).
exists y; apply: ord_leA; split => // t tx; apply /setU1_P.
case: (ordinal_trichotomy (ordinal_hi ox yx)(ordinal_hi ox tx)); fprops.
by move => yt; move: (setU_i yt tx).
Qed.

a limit ordinal is a non-successorr; it contains zero and is stable by succ_o; it is the supremum of all elements smaller than itself

Definition limit_ordinal x:=
  [/\ ordinalp x, inc \0o x & (forall y, inc y x -> inc (succ_o y) x)].

Lemma limit_ordinal_P1 x: ordinalp x ->
  ((limit_ordinal x) <-> (nonempty x /\ x = union x)).
Proof.
move=> ox.
move: (ordinal_irreflexive ox) => ir.
split.
  move=> [_ nex p]; split; first by exists emptyset.
  case: (proj1 (osuccVidpred ox)) => // [] [y oy xy].
  have yx: (inc y x) by ord_tac.
  by move: (p _ yx); rewrite -xy => bad.
move=> [nex xu]; split=>//.
   by move: (ord_ne_pos ox nex)=> h; ord_tac.
move=> y yx; move: (ordinal_hi ox yx)=> oy.
case: (ordinal_trichotomy (OS_succ oy) ox) =>//.
  case /setU1_P => h; last by rewrite -h in yx.
  by move:((ordinal_transitive ox yx) _ h).
move: (osuccVidpred ox)=> [ _ dj] h.
case: dj; split => //; by exists y.
Qed.

Lemma limit_ordinal_pr2 x: ordinalp x ->
  [\/ x = \0o, succ_op x | limit_ordinal x].
Proof.
move=> ox.
case: (emptyset_dichot x); first by constructor 1.
move=> nex.
move: (osuccVidpred ox) => [h _]; case: h; first by constructor 2.
by move=> xu; constructor 3; apply /(limit_ordinal_P1 ox).
Qed.

Lemma limit_ordinal_P3 x:
  limit_ordinal x <->
  (\0o <o x /\ forall t, t <o x -> succ_o t <o x).
Proof.
split.
  move => [ox xnz xl]; split.
  + by apply: (ord_ne0_pos ox) => xz; move: xnz; rewrite xz; move/in_set0.
  + by move => t /(ord_ltP ox) => h; apply/(ord_ltP ox); apply: xl.
move => [[[_ ox sa] xnz] sb]; split => //.
+ apply: ord_ne_has0; fprops.
+ by move => t /(ord_ltP ox) => h; apply/(ord_ltP ox); apply: sb.
Qed.

Lemma succo_K y: ordinalp y -> \opred (succ_o y) = y.
Proof.
move=> oy; set_extens t => ts; last by apply: (setU_i ts); fprops.
move: (setU_hi ts) => [a ta]; case /setU1_P;last by move => <-.
move => ay; ord_tac0.
Qed.

Lemma predo_K x: ordinalp x -> succ_op x -> succ_o (\opred x) = x.
Proof.
by move=> ox [y oy xs]; rewrite xs (succo_K oy).
Qed.

If from two equipotent sets we remove an element, we get equipotent sets

Section SuccProp.
Variables (x y a b: Set).
Hypotheses (nax: ~ inc a x) (nby: ~ inc b y).

Lemma setU1_injective_card2:
   ((x +s1 a) \Eq (y +s1 b) <-> x \Eq y).
Proof.
split; last first.
  move=> [f [ [[ff injf] srjf] sf tf]].
  have sjt: surjection (extension f a b) by apply: extension_fs =>//;ue.
  have st: source (extension f a b) = x +s1 a by rewrite /extension; aw;ue.
  have tt: target (extension f a b) = y +s1 b by rewrite /extension; aw;ue.
  have asf: ~ inc a (source f) by ue.
  exists (extension f a b); split => //.
   split => //; split; first by fct_tac.
   rewrite st; move=> u v; case /setU1_P=> us; case /setU1_P => vs.
   + rewrite ! extension_Vf_in //; try ue; apply: injf; ue.
   + rewrite (extension_Vf_in _ ff asf); last by ue.
     rewrite vs (extension_Vf_out _ ff asf);move =>h;case:nby;rewrite -h; Wtac.
   + rewrite us(extension_Vf_out _ ff asf)(extension_Vf_in _ ff asf);last by ue.
     move =>h; case: nby; rewrite h; Wtac.
   + rewrite us vs !extension_Vf_out //.
move=> [f [[[ff injf] sjf] sf tf]].
have yt: inc b (target f) by rewrite tf; fprops.
move: ((proj2 sjf) _ yt) => [a' asf Wa].
set g := Lf (fun z => Yo (z = a') (Vf f a) (Vf f z)) x y.
exists g; rewrite /g;split => //; aw.
have xsf: inc a (source f) by rewrite sf; fprops.
have sxsf: sub x (source f) by rewrite sf; move=> t; fprops.
apply: lf_bijective.
    move=> z bx; simpl; Ytac ba.
      move: (Vf_target ff xsf); rewrite tf.
      case /setU1_P => // h; rewrite - h in Wa; move: (injf _ _ asf xsf Wa).
      by move=> ab; case: nax; rewrite -ab - ba.
    have bsf: inc z (source f) by rewrite sf; fprops.
    move: (Vf_target ff bsf); rewrite tf.
    case /setU1_P => // h; rewrite -h in Wa; move: (injf _ _ asf bsf Wa).
    by move=> ab; case: ba.
  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 case: nax; rewrite -aux.
move=> z zt.
have ztf: (inc z (target f)) by rewrite tf ;fprops.
case: (equal_or_not z (Vf f a)) => zW.
  rewrite zW; exists a' => //; last by Ytac0.
  move: asf; rewrite sf; case /setU1_P => //.
  move=> ax;move: zt; rewrite zW -{1} ax Wa => nyy; contradiction.
move: ((proj2 sjf) _ ztf) => [b' bsf Wb].
case: (equal_or_not b' a') => ba.
  by move: nby; rewrite - Wa - ba Wb.
exists b'; last by Ytac0.
move: bsf; rewrite sf; case /setU1_P => // bx.
by case: zW; rewrite -Wb bx.
Qed.

this says that a superset of an infinite set is infinite

Lemma setU1_injective_card1:
  sub x y -> x \Eq (x +s1 a) -> y \Eq (y +s1 b).
Proof.
move=> sxy aux.
have nbx: ~ inc b x by dneg bx; apply: sxy.
move: (equipotentS aux)=> [f [[[ff injf] sjf] sf tf]].
eqsym; clear aux.
have Asf: inc a (source f) by rewrite sf; fprops.
have wafx: inc (Vf f a) x by Wtac.
set g := fun z => Yo (inc z x) (Vf f z) (Yo (z = b) (Vf f a) z).
have Byp: forall t, inc t y -> t <> b by move=> t ty tB; case: nby; ue.
have pa: lf_axiom g (y +s1 b) y.
  move=> t /setU1_P; rewrite /g; case.
    move=> ty; Ytac tx; first by apply: sxy; Wtac; rewrite sf; fprops.
    by move: (Byp _ ty) => aux; Ytac0.
  by move => ->; Ytac0; Ytac0; apply: sxy.
have pb: forall u v, inc u (y +s1 b) -> inc v (y +s1 b) -> g u = g v -> u = v.
  move=> u v; rewrite /g; case /setU1_P => uy /setU1_P aux; last first.
    rewrite uy; Ytac0; Ytac0; Ytac 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.
  Ytac ux.
    Ytac vx; first by apply: injf; rewrite sf; fprops.
    case: aux => vy.
      move: (Byp _ vy) => aux; Ytac0=> h; case: vx; rewrite -h -tf.
      Wtac; rewrite sf; fprops.
    Ytac0 => aux.
    have usf: inc u (source f) by rewrite sf; fprops.
    by rewrite (injf _ _ usf Asf aux) in ux.
  have uB: u <> b by move => ub; case: nby; ue.
  Ytac0; Ytac vx.
      move=> h; rewrite h in ux; case: ux; rewrite -tf.
      Wtac; rewrite sf; fprops.
  case: aux => vy; [move: (Byp _ vy) => aux |]; Ytac0 => //.
  move=> h;case: ux; ue.
exists (Lf g (y +s1 b) y); split; aw; apply: lf_bijective => //.
move=> t ty.
case: (inc_or_not t x) => tx.
  rewrite -tf in tx; move: ((proj2 sjf) _ tx)=> [z zsf wz].
  move: zsf; rewrite sf;case /setU1_P => zx.
    exists z; first by apply /setU1_P; left; apply: sxy.
    by rewrite /g; Ytac0.
  by exists b; fprops; rewrite /g; Ytac0; Ytac0; rewrite - zx wz.
by move: (Byp _ ty) => aux;exists t; fprops;rewrite /g; Ytac0; Ytac0.
Qed.

End SuccProp.

We say that x is infinite if equipotent to its successor; finite otehrwise; note that ordinalp x is missing in the definition of infinite

Definition infinite_o u := u \Eq (succ_o u).
Definition finite_o u := ordinalp u /\ ~ (infinite_o u).

Lemma infinite_o_increasing x y: ordinalp x -> ordinalp y ->
  inc x y -> infinite_o x -> infinite_o y.
Proof.
rewrite /infinite_o; move=> ox oy xy.
apply: setU1_injective_card1 (ordinal_irreflexive ox)
  (ordinal_irreflexive oy) (ordinal_transitive oy xy).
Qed.

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

Lemma succ_injective_oP x y: ordinalp x -> ordinalp y ->
  ((succ_o x) \Eq (succ_o y) <-> x \Eq y).
Proof.
move=> ox oy.
apply: setU1_injective_card2 (ordinal_irreflexive ox) (ordinal_irreflexive oy).
Qed.

Lemma infinite_oP x: ordinalp x ->
  (infinite_o (succ_o x) <-> infinite_o x).
Proof. move=> ox; apply/ (succ_injective_oP ox (OS_succ ox)). Qed.

Lemma finite_oP x: finite_o (succ_o x) <-> finite_o x.
Proof.
split.
  move=> [p1 p2].
  have ox: ordinalp x by apply: OS_succr.
  by move: p2 => /(infinite_oP ox) => h; split.
by move=> [p1 p2]; split; [ apply: OS_succ | move/(infinite_oP p1)].
Qed.

limit ordinals are infinite, since succ_o is a bijecion for the least infinite ordinal

Lemma limit_infinite x: limit_ordinal x -> infinite_o x.
Proof.
move=> xl.
have ox:= (proj31 xl).
move: (least_ordinal1 ox xl).
set A := least_ordinal limit_ordinal x.
move=> [oA [_ eA liA] leA].
suff p: (infinite_o A).
  case: (ordinal_sub oA ox (leA _ ox xl)) => Ax; first by ue.
  apply: (infinite_o_increasing oA ox Ax p).
move: (ordinal_irreflexive oA) => nAA.
pose f z := Yo (inc z A) (succ_o z) emptyset.
eqsym;exists (Lf f (succ_o A) A); split => //; aw.
have q1: forall z, inc z (succ_o A) -> inc (f z) A.
  by move=> u; case /setU1_P => hu; rewrite /f ?hu ; Ytac0 => //; apply: liA.
apply: lf_bijective => //.
  move=> u v; rewrite /f; case /setU1_P => uA; [ | rewrite uA] => vA; Ytac0;
    case /setU1_P: vA => vA; rewrite ? vA; Ytac0.
  - move=> eq.
     have:inc u (succ_o u) by fprops.
     have:inc v (succ_o v) by fprops.
    rewrite eq - {1} eq;case /setU1_P => // uv; case /setU1_P => // vu.
      case: (ordinal_asymmetric oA uA vA vu uv).
  - move=> bad; empty_tac1 u.
  - move=> bad; symmetry in bad; empty_tac1 v.
  - done.
set z':= Zo A (fun z=> ~ (exists2 x0, inc x0 (succ_o A)& z = f x0)).
case: (emptyset_dichot z') => nez.
  move=> y yA; ex_middle bad;empty_tac1 y; apply: Zo_i => //.
have alo': ordinal_set z' by move => a /Zo_P [aA _]; ord_tac.
move: (ordinal_setI nez alo').
set B:= intersection z';move => iz'.
move: (iz') => /Zo_P [r1 r2].
move: (ordinal_hi oA r1) => oB.
case: (emptyset_dichot B) => be.
  by case: r2; exists A => //; fprops; rewrite /f Y_false.
suff aux: (limit_ordinal B).
  move: ((leA _ oB aux) _ r1) => sab.
  by case: (ordinal_irreflexive oB).
apply/(limit_ordinal_P1 oB); split =>//.
move: (osuccVidpred oB) => [ca _ ]; case: ca =>//; move=> [y oy ta].
have yB: inc y B by rewrite ta; fprops.
have yA: inc y A by apply: (ordinal_transitive oA r1 yB).
have yAA: inc y (succ_o A) by rewrite /succ_o;fprops.
have fy: f y = B by rewrite ta /f; Ytac0.
case: r2; ex_tac.
Qed.

The cardinal of x is the least ordinal equipotent to x

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

Definition cardinalV_prop x y :=
  [/\ ordinalp y, x \Eq y &
  (forall z, ordinalp z -> x \Eq z -> sub y z)].

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

Lemma cardinalV_pr0 x: cardinalV_prop x (cardinalV x).
Proof.
move: (Zermelo_ter x)=> [wor sr].
move: (ordinal_isomorphism_exists wor) => [or oi].
set f :=(ordinal_iso (worder_of x)) in or oi.
have extf: x \Eq (ordinal (worder_of x)).
  move : oi => [_ _ [bf sf tf] ff]; exists f; first by split => //; ue.
apply: (least_ordinal1 or extf).
Qed.

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

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

Notation cardinal := Cardinal.cardinal.
Definition cardinalp x:=
 ordinalp x /\ (forall z, ordinalp z -> x \Eq z -> sub x z).
Definition cardinal_fam x := allf x cardinalp.
Definition cardinal_set X := alls X cardinalp.

Lemma cardinalV_pr x: cardinalV_prop x (cardinal x).
Proof. by rewrite Cardinal.cardinalE; apply /cardinalV_pr0. Qed.

Lemma card_card x: cardinalp x -> cardinal x = x.
Proof.
move=> [cx1 cx2].
have aux: cardinalV_prop x (cardinal x) by apply: cardinalV_pr.
have aux': cardinalV_prop x x by split; fprops.
apply: (cardinalV_unique aux aux').
Qed.

Ltac eq_aux:= match goal with
  H: cardinalp ?a |- cardinal ?b = ?a => rewrite- (card_card H); aw
| H: cardinalp ?a |- ?a = cardinal ?b => rewrite- (card_card H); aw
end.

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

Lemma OS_cardinal x: cardinalp x -> ordinalp x.
Proof. by move=> [ox _]. Qed.

Hint Resolve CS_cardinal: fprops.

Lemma double_cardinal x: cardinal (cardinal x) = cardinal x.
Proof. apply: card_card; fprops. Qed.

Lemma cardinal_pr0 x: x \Eq (cardinal x).
Proof. exact: (proj32 (cardinalV_pr x)). Qed.

Lemma cardinal_pr x: (cardinal x) \Eq x.
Proof. by eqsym; apply: cardinal_pr0. Qed.

Lemma cardinal_ordinal_le x: ordinalp x -> cardinal x <=o x.
Proof.
move => ox.
move: (cardinalV_pr x) => [pa pb pc]; split; fprops.
Qed.

Hint Resolve cardinal_pr0 cardinal_pr: fprops.

Theorem card_eqP x y:
   (cardinal x = cardinal y) <-> (x \Eq y).
Proof.
split => 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.

Lemma cardinalP x:
  cardinalp x <-> (ordinalp x /\ forall z, inc z x -> ~ (x \Eq z)).
Proof.
rewrite /cardinalp; split; move=> [ox h]; split => //.
  move => z zx ne; move: ((h _ (ordinal_hi ox zx) ne) _ zx).
  apply: (ordinal_decent ox zx).
move=> z oz exz.
case: (ordinal_trichotomy oz ox) => ty; first by case: (h _ ty).
  by apply: (ordinal_transitive oz).
by rewrite ty.
Qed.

Lemma cardinal_image f x :
  sub x (source f) -> injection f ->
  cardinal (image_by_fun f x) = cardinal x.
Proof. by move => pa /(equipotent_restriction1 pa)/card_eqP. Qed.

Lemma cardinal_range f: injection f ->
  cardinal (range (graph f)) = (cardinal (source f)).
Proof. by move /equipotent_range /card_eqP. Qed.

Lemma cardinal_indexed a b: cardinal (a *s1 b) = cardinal a.
Proof. symmetry;apply /card_eqP; apply:equipotent_indexed. Qed.

Lemma cardinal_indexedr a b: cardinal (indexedr b a) = cardinal a.
Proof. symmetry;apply /card_eqP; apply:equipotent_rindexed. Qed.


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

Definition ord_one := card_one.
Definition ord_two := card_two.

Notation "\0c" := card_zero.
Notation "\1c" := card_one.
Notation "\2c" := card_two.
Notation "\1o" := ord_one.
Notation "\2o" := ord_two.

Lemma succ_o_zero: succ_o \0o = \1o.
Proof.
set_extens z.
   move/setU1_P; case; [ case; case | move => ->//; apply:set1_1].
move /set1_P => ->; fprops.
Qed.

Lemma succ_o_one: succ_o \1o = \2o.
Proof.
set_extens z.
  case/setU1_P; [move/set1_P => ->; apply/set2_1 | move => ->; apply/set2_2].
by case /set2_P => h; apply /setU1_P; [left; apply /set1_P | right].
Qed.

Lemma constants_v: (C0 = \0c /\ C1 = \1c /\ C2 = \2c).
Proof. by []. Qed.

Lemma OS1: ordinalp \1o.
Proof. rewrite - succ_o_zero; apply: OS_succ; apply: OS0. Qed.

Lemma OS2: ordinalp \2o.
Proof. rewrite - succ_o_one; apply: OS_succ; apply: OS1. Qed.

Lemma equipotent_to_emptyset x: x \Eq emptyset -> x = emptyset.
Proof.
move=> [y [[[fy _] suy] sy ty]].
apply /set0_P => z zx; empty_tac1 (Vf y z); Wtac.
Qed.

Lemma cardinal_set0: cardinal emptyset = \0c.
Proof. apply: equipotent_to_emptyset; apply: (cardinal_pr emptyset). Qed.

Lemma cardinal_nonemptyset x:
  cardinal x = \0c -> x = emptyset.
Proof.
rewrite - cardinal_set0; move /card_eqP.
apply: equipotent_to_emptyset.
Qed.

Lemma cardinal_nonemptyset0 x: x <> \0c -> cardinal x <> \0c.
Proof. by move => pa pb; case: pa; apply: cardinal_nonemptyset. Qed.

Lemma cardinal_nonemptyset1 x:
  nonempty x -> cardinal x <> \0c.
Proof. by move=> nex; apply :cardinal_nonemptyset0; apply /nonemptyP. Qed.

Lemma card1_nz: \1c <> \0c.
Proof. exact: TP_ne1. Qed.

Lemma card2_nz: \2c <> \0c.
Proof. exact: (proj1 C2_neC01). Qed.

Lemma card_12: \1c <> \2c.
Proof. exact: (nesym (proj2 C2_neC01)). Qed.

Hint Resolve card_12 card1_nz card2_nz: fprops.

Zero is finite as well as its sucessors

Lemma finite_zero: finite_o \0o.
Proof.
split; first by apply: OS0.
move=> h; move: (equipotentS h); rewrite /card_zero=> h'.
move: (equipotent_to_emptyset h') => h''.
have [[]]: inc \0o emptyset by rewrite - h'' /succ_o; fprops.
Qed.

Lemma finite_one: finite_o \1o.
Proof. rewrite - succ_o_zero; apply /finite_oP; apply:finite_zero. Qed.

Lemma finite_two: finite_o \2o.
Proof. by rewrite - succ_o_one; apply /finite_oP; apply:finite_one. Qed.

Lemma finite_succ x:
  finite_o x <-> (x = emptyset \/ (exists2 y, finite_o y & x = succ_o y)).
Proof.
split.
  move => fx; move: (fx) => [ox nix].
  case: (limit_ordinal_pr2 ox); first by left.
    move=> [y oy xK]; rewrite xK; right; exists y => //.
     by move: fx; rewrite xK; move /finite_oP.
  move=> h; case: nix;apply: (limit_infinite h).
case; first by move => ->; apply: finite_zero.
by move=> [y fy ->];apply/finite_oP.
Qed.

If there is injections E->F and F->E, then there are bijections; We start with the case sub F E

Lemma Cantor_Bernstein1 E F f:
  sub F E ->
  (forall x, inc x E -> inc (f x) F) ->
  {inc E &, injective f} ->
  E \Eq F.
Proof.
move=> 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: Zo_S.
set (B:= E -s F).
set (C:= Zo A (fun x=> sub B x)).
have EC: inc E C.
   apply: Zo_i;[ apply: Zo_i; fprops;apply :setP_Ti | apply: sub_setC].
set (D:= intersection C).
have p1: forall x, inc x C -> sub D x.
  move=> x xC; rewrite /D=> t tD; apply: (setI_hi tD xC).
have DA: inc D A.
  rewrite /A; apply: Zo_i.
    by apply /setP_P; apply: setI_s1.
   move=> y yD; apply: setI_i; first by ex_tac.
   move=> t tC; move: (setI_hi yD tC) => yt.
   by move: tC => /Zo_P [] /Zo_hi tp _; apply: tp.
have DC: inc D C.
   apply: Zo_i => //t tD; apply /setI_i ; first by ex_tac.
   by move=> y /Zo_P [_]; apply.
have BD: sub B D by move: DC => /Zo_P [].
have cEB: (E -s B = F) by apply: setC_K.
have Dst: (forall y, inc y D -> inc (f y) D) by move: DA => /Zo_P [].
exists (Lf (fun y => Yo (inc y D) (f y) y) E F).
aw;split => //; aw; apply: lf_bijective.
    move=> y yE /=; Ytac yD; first by apply: tf.
    rewrite -cEB; apply/setC_P; split => //; fprops.
  move=> u v uE vE; Ytac uD; Ytac vD => //; try (apply: fi => //).
    by move=> h; rewrite -h in vD; case: vD; apply: Dst.
  by move=> h; rewrite h in uD; case: uD; apply: Dst.
move=> y yF; move: (yF); rewrite -cEB => /setC_P [yE nyB].
case: (inc_or_not y D) => yD; last by exists y => //; Ytac0.
have DE:sub D E by move: DA => /Zo_P [] /setP_P.
set (T:= D -s1 y).
have BT: sub B T.
  by move=> t tB; apply /setC1_P; split; [ apply: BD | dneg ty; rewrite -ty].
have TA: (~ (inc T A)).
  move=> TA.
  have TC: (inc T C) by apply: Zo_i.
  by move: ((p1 _ TC) _ yD) => /setC1_P [_].
have [x xT nfT]: exists2 x, inc x T & ~ (inc (f x) T).
  ex_middle bad; case: TA;apply: Zo_i => //.
    apply /setP_P; apply: sub_trans DE; apply: sub_setC.
  move=> z zT; case: (inc_or_not (f z) T) => //; move => nfzt; case:bad; ex_tac.
move: xT => /setC1_P [xD nxy].
exists x; first by apply: DE.
Ytac0;ex_middle fxy; case: nfT; apply /setC1_P; split; fprops.
Qed.

Theorem CantorBernstein X Y:
  (exists f, injection_prop f X Y) ->
  (exists f, injection_prop f Y X) ->
  (exists f, bijection_prop f X Y).
Proof.
move=> [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.
suff e2: X \Eq Z.
  have //: X \Eq Y by eqtrans Z; eqsym.
set g:= fun w => Vf (Vf w f1) f2.
have ff2: function f2 by fct_tac.
have ff1: function f1 by fct_tac.
move: (f_range_graph ff2) => rg2.
move: (image_by_fun_source ff2); rewrite /image_of_fun sf2 -/Z => zv.
apply: (Cantor_Bernstein1).
- rewrite zv -tf2; apply f_range_graph; fct_tac.
- move=> x xs.
  apply/(Vf_image_P ff2); first by rewrite - sf2;fprops.
  exists (Vf f1 x) => //;Wtac.
- rewrite - sf1 /g; move=> x y xs ys sg.
  move: if1 => [_ prop]; apply: prop => //.
  move: if2 => [_ prop2].
  apply: prop2 => //;rewrite sf2 -tf1;Wtac.
Qed.

a finite ordinal is a cardinal ; so zero, one and two are cardinals

Lemma CS_succ_o x: finite_o x -> cardinalp (succ_o x).
Proof.
move=> [ox nix]; apply/cardinalP; split; first by apply: OS_succ.
move=> z zo.
dneg aux1; eqtrans z; last by eqsym.
have zx: (sub z x).
  move: zo;case /setU1_P; [apply: (ordinal_transitive ox) | move=> ->; fprops].
move: (ordinal_irreflexive ox) => xx.
move: aux1 => [g [[[fg injg] sjg] sg tg]].
pose f z := Vf g z.
have p1: (forall t, inc t x -> inc (f t) z).
  by rewrite -tg /f=>t tx; Wtac; rewrite sg; apply: setU1_r.
have p2:(forall u v, inc u x -> inc v x -> f u = f v -> u = v).
  by rewrite /f => u v uE vE; apply: injg; rewrite sg ;apply: setU1_r.
apply: (Cantor_Bernstein1 zx p1 p2).
Qed.

Lemma CS0: cardinalp \0c.
Proof.
apply/cardinalP; split; [by apply: OS0 | move=> z;case; case].
Qed.

Lemma CS_finite_o x: finite_o x -> cardinalp x.
Proof.
rewrite finite_succ; case.
  move => ->; apply: CS0.
by move=> [y yF ->]; apply: CS_succ_o.
Qed.

Lemma CS1: cardinalp \1c.
Proof. apply:CS_finite_o; apply:finite_one. Qed.

Lemma CS2: cardinalp \2c.
Proof. apply:CS_finite_o; apply:finite_two. Qed.

Hint Resolve CS0 CS1 CS2 : fprops.

We define finite and infinite for sets and cardinals

Definition finite_c := finite_o.
Definition infinite_c a := cardinalp a /\ infinite_o a.
Definition finite_set E := finite_c (cardinal E).
Definition infinite_set E := infinite_o (cardinal E).

Lemma infinite_pr1 y z: infinite_c z ->
  z = succ_o y -> False.
Proof.
move => [] /cardinalP [c1 c2] iz zyy.
rewrite zyy in c1 c2 iz.
have yz: (inc y (succ_o y)) by fprops.
move: (ordinal_hi c1 yz) => /(infinite_oP) h; move /h: iz => io.
by case: (c2 _ yz); eqsym.
Qed.

Lemma infinite_dichot1 x: finite_c x -> infinite_c x -> False.
Proof. by move=> [_ pa][_ pb]. Qed.

Lemma CS_finite2 x: finite_c x -> cardinalp x.
Proof. by apply: CS_finite_o. Qed.

Hint Resolve CS_finite2: fprops.

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

Lemma infinite_nz y: infinite_c y -> y <> \0c.
Proof.
move =>iy h; rewrite h in iy;case: (infinite_dichot1 finite_zero iy).
Qed.

We define here the cardinal successor

Definition succ x := cardinal (succ_o x).

Lemma CS_succ a: cardinalp (succ a).
Proof. rewrite /succ; fprops. Qed.

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

Theorem succ_injective1: {when cardinalp &, injective succ}.
Proof.
move=> a b ca cb; move /card_eqP.
move: (CS_cardinal a) (CS_cardinal b) => cca ccb.
move /(setU1_injective_card2(cardinal_irreflexive ca)(cardinal_irreflexive cb)).
move /card_eqP; rewrite ! card_card //.
Qed.

Lemma card_succ_pr a b: ~ (inc b a) ->
  cardinal (a +s1 b) = succ (cardinal a).
Proof.
move=> bna; apply /card_eqP.
apply /setU1_injective_card2 => //;last by fprops.
apply: cardinal_irreflexive; fprops.
Qed.

Lemma card_succ_pr1 a b:
  cardinal ((a -s1 b) +s1 b) = succ (cardinal (a -s1 b)).
Proof. rewrite card_succ_pr //; apply: setC1_1. Qed.

Lemma card_succ_pr2 a b: inc b a ->
  cardinal a = succ (cardinal (a -s1 b)).
Proof. move=> ba; rewrite - {1} (setC1_K ba); apply: card_succ_pr1. Qed.

Lemma infinite_set_pr a b: inc b a -> a \Eq (a -s1 b) ->
  infinite_set a.
Proof.
move=> ba /card_eqP eq; apply/card_eqP; rewrite double_cardinal.
move: (card_succ_pr2 ba); rewrite -eq /succ //.
Qed.

Lemma infinite_set_pr1 a b: inc b a ->
  a \Eq (a -s1 b) -> infinite_set (a -s1 b).
Proof.
move=> ab => h.
move: (infinite_set_pr ab h).
by move /card_eqP:h; rewrite /infinite_set; move => <-.
Qed.

Lemma infinite_set_pr2 x: infinite_o x -> ~(inc x x) -> infinite_set x.
Proof.
rewrite /infinite_o/succ_o => eq1 eq2.
set (a:= (x +s1 x)).
move: (equipotentS eq1) => eq3.
have eq : a -s1 x = x by apply: setU1_K.
rewrite - eq; apply: infinite_set_pr1 ; [ rewrite /a; fprops | ue ].
Qed.

We exhibit an infinite set

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:= triple nat (nat -s1 (Ro 0)) (gacreate S).
have gf: graph f = (gacreate S) by rewrite /f; aw.
have p0: fgraph (gacreate S).
  split.
    move=> t /IM_P [a <-]; fprops.
  move=> x y /IM_P [a <-] /IM_P [b <-]; aw => sp.
  by rewrite sp (R_inj sp).
have p1: sgraph (gacreate S) by fprops.
have p2:nat = domain (gacreate S).
  set_extens t.
    move=> tn; apply/(domainP p1); exists (Ro (S (Bo tn))).
    apply/IM_P; exists (Bo tn); by rewrite B_eq.
  move=> /(domainP p1) [y] /IM_P [a Je]; rewrite -(pr1_def Je); apply: R_inc.
have p3: (range (gacreate S))= (nat -s1 (Ro 0)).
  set_extens t.
    move => /(rangeP p1) [x] /IM_P [a Jeq].
    rewrite -(pr2_def Jeq); apply/setC1_P; split; first by apply: R_inc.
    by move=> h; move:(R_inj h).
  move=> /setC1_P [tn to]; apply/(rangeP p1).
  have [w wp]: exists w:nat, t = Ro w by exists (Bo tn); rewrite (B_eq tn).
  have: w <> 0 by dneg xx; ue.
  rewrite wp;clear to wp.
  case: w => // n _; exists (Ro n); apply/IM_P; exists n =>//.
have ff: function f.
  apply: function_pr =>//; rewrite p3; fprops.
have sf: surjection f by apply: surjective_pr4 =>//;rewrite /f; aw.
exists f; rewrite /f;red;aw; split => //; split => //.
apply: injective_pr_bis =>//.
move=> x x' y; rewrite /related gf => /IM_P [a J1] /IM_P [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).
Qed.

We consider here the least infinite ordinal; It is an infinite cardinal

Definition omega0 := least_ordinal infinite_o (cardinal nat).

Lemma omega0_pr:
   [/\ ordinalp omega0, infinite_o omega0 &
   (forall z, ordinalp z -> infinite_o z -> sub omega0 z)].
Proof.
have p1: ordinalp (cardinal nat).
  by move: (CS_cardinal nat) => [ok _].
by move: (least_ordinal1 p1 nat_infinite_set).
Qed.

Lemma OS_omega: ordinalp omega0.
Proof. by move: omega0_pr => [h _ ]. Qed.

Hint Resolve OS0 OS1 OS2 OS_omega : fprops.

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

Lemma omega_P1 x: ordinalp x ->
  (infinite_o x <-> sub omega0 x).
Proof.
move=> ox; split; first by move: omega0_pr => [_ _ h]; apply: h.
move: omega_infinite OS_omega => bi oo sox.
case: (ordinal_sub oo ox sox); first by move => <- //.
move=> h; apply: (infinite_o_increasing oo ox h bi).
Qed.

Lemma omega_P2 x: inc x omega0 <-> finite_o x.
Proof.
move: OS_omega => oo.
split => xo.
  have ox:= (ordinal_hi oo xo).
  split=>//; move /(omega_P1 ox) => h.
  case: (ordinal_irreflexive ox (h _ xo)).
move: xo => [ox nifx].
by case:(ord_le_to_si oo ox) => // /(omega_P1 ox).
Qed.

Lemma CS_omega: cardinalp omega0.
Proof.
move: OS_omega => oo;split => // => z oz pa; apply /(omega_P1 oz).
move: omega_infinite => h.
eqtrans (succ_o omega0); first by eqtrans omega0; eqsym.
by apply /succ_injective_oP.
Qed.

Lemma omega_infinitec: infinite_c omega0.
Proof. split; [ apply: CS_omega | apply: omega_infinite]. Qed.

Lemma omega_limit0: omega0 = \opred omega0.
Proof.
case (proj1 (osuccVidpred OS_omega)) =>//.
move=> [y oy ys].
have : inc y omega0 by rewrite ys ; fprops.
move => /omega_P2 /finite_oP; rewrite -ys; move => [_[]].
apply: omega_infinite.
Qed.

Lemma omega_limit: limit_ordinal omega0.
Proof.
apply/(limit_ordinal_P1 OS_omega).
split; last by apply: omega_limit0.
exists \0c; apply /omega_P2; apply: finite_zero.
Qed.

Lemma omega_limit2 x: limit_ordinal x -> omega0 <=o x.
Proof.
move=> h; move: (h) => [Bx _]; split; fprops.
apply/(omega_P1 Bx); apply: (limit_infinite h).
Qed.

Some properties of infinite sets

Lemma infinite_card_limit1 x: infinite_c x -> \opred x = x.
Proof.
move => icx.
move: (osuccVidpred (OS_cardinal (proj1 icx))) => [p3 _].
case: p3 => // [] [y _ h]; case: (infinite_pr1 icx h).
Qed.

Lemma infinite_card_limit2 x: infinite_c x -> limit_ordinal x.
Proof.
move => ic; move: (ic) => [p1 p2].
apply /(limit_ordinal_P1 (OS_cardinal p1)).
split; last by symmetry;apply: infinite_card_limit1.
by case: (emptyset_dichot x) => // xe; case: (infinite_nz ic).
Qed.

Lemma omega_limit3 x: infinite_c x -> sub omega0 x.
Proof.
by move=> h; move: (omega_limit2 (infinite_card_limit2 h)) => [_].
Qed.

Lemma infinite_setP x: infinite_set x <-> infinite_c (cardinal x).
Proof.
by move: (CS_cardinal x) => h; split; [ move => h1 | move => [] ].
Qed.

Lemma infinite_set_pr3 x: omega0 <=o x -> infinite_c (cardinal x).
Proof.
move => [p1 p2 p3].
apply /infinite_setP;apply: infinite_set_pr2.
  apply /omega_P1 => //.
exact (ordinal_irreflexive p2).
Qed.

End Bordinal.

Export Bordinal.

Module Cardinal.

EIII-3-1 The cardinal of a set

Singletons are equipotent, as well as doubletons

Lemma set1_equipotent x y:
  singleton x \Eq singleton y.
Proof.
move: (set1_order_is x y) => [f [_ _ [pa pb pc] _]].
move: pb pc;rewrite (proj2 (set1_wor x)) (proj2 (set1_wor y)) => <- <-.
by exists f.
Qed.

Lemma cardinal_set1 x: cardinal (singleton x) = \1c.
Proof. rewrite -(card_card CS1); apply /card_eqP; apply: set1_equipotent. Qed.

Lemma set2_equipotent1 x y: x <> y ->
   exists g, [/\ bijection_prop g (doubleton x y) C2,
     Vf g x = C0 & Vf g y = C1].
Proof.
move => neq.
have ax: lf_axiom (fun z => Yo (z = x) C0 C1) (doubleton x y) C2.
   by move => t tp; apply /set2_P; Ytac h; [left | right].
exists (Lf (fun z => Yo (z = x) C0 C1 ) (doubleton x y) C2).
split; aw; fprops; try Ytac0 =>//.
split; aw;apply: lf_bijective.
    done.
  move=> u v /set2_P [] -> /set2_P [] ->; Ytac0 => //; Ytac0 => // => h.
  by case: TP_ne.
  by case: TP_ne1.
by move => z; case/C2_P => ->; [exists x | exists y]; fprops; Ytac0.
Qed.

Lemma set2_equipotent x y: x <> y -> doubleton x y \Eq \2c.
Proof. by move => /set2_equipotent1 [g [bg sg tg]]; exists g. Qed.

Lemma cardinal_set2 x x': x <> x' -> cardinal (doubleton x x') = \2c.
Proof.
move=> xx'; rewrite -(card_card CS2).
by apply /card_eqP /set2_equipotent.
Qed.

Lemma set_of_card_one x: cardinal x = \1c -> singletonp x.
Proof.
move=> xh; symmetry in xh; move: xh.
rewrite -(card_card CS1); move /card_eqP; rewrite /card_one.
move=> [f [[[ff injf] sf] srf tf]]; exists (Vf f emptyset).
rewrite -tf.
have p1: inc (Vf f emptyset) (target f) by Wtac; rewrite srf;fprops.
set_extens t; last by move /set1_P => ->.
move=> tx; move: ((proj2 sf) _ tx)=> [y]; rewrite srf.
move=> /set1_P -> <-; fprops.
Qed.

Lemma set_of_card_two x: cardinal x = \2c -> doubletonp x.
Proof.
move=> xh; symmetry in xh; move: xh.
rewrite -(card_card CS2); move /card_eqP; rewrite / card_two.
move=> [f [[[ff injf] sf] srf tf]].
have es: inc emptyset (source f) by rewrite srf; fprops.
have ses: inc (singleton emptyset) (source f) by rewrite srf; fprops.
exists (Vf f emptyset); exists (Vf f (singleton emptyset)); split.
  by move=> aux; move: (injf _ _ es ses aux); fprops.
rewrite -tf; set_extens t => ts.
  move: ((proj2 sf) _ ts) => [z zsf <-].
  move: zsf; rewrite srf; case /set2_P => ->; fprops.
case /set2_P: ts => ->; Wtac.
Qed.

Equipotency is compatible with products

Definition equipotent_ex E F :=
   choose (fun z=> bijection_prop z E F).

Lemma equipotent_ex_pr E F:
  E \Eq F -> bijection_prop (equipotent_ex E F) E F.
Proof. move => e; apply: (choose_pr e). Qed.

Definition fgraphs_equipotent x y :=
  domain x = domain y
  /\ (forall i, inc i (domain x) -> (Vg x i) \Eq (Vg y i)).

Lemma equipotent_setXb x y:
  fgraphs_equipotent x y -> (productb x) \Eq (productb y).
Proof.
move=> [dxy ale].
pose g i := equipotent_ex (Vg x i) (Vg y i).
pose f i := graph (g i).
rewrite -(productb_gr x) - (productb_gr y) - dxy.
exists (ext_map_prod (domain x) (Vg x) (Vg y) f).
red; rewrite /ext_map_prod; split;aw.
have ea: ext_map_prod_axioms (domain x) (Vg x) (Vg y) f.
  move=> i iI; move: (equipotent_ex_pr (ale _ iI))=> [[[fg _] _] sg tg].
  rewrite /f; split; fprops.
    by rewrite - sg; apply: f_domain_graph.
  by rewrite -tg;apply: f_range_graph.
split.
  apply: ext_map_prod_fi =>//.
  move=> i iI; move: (equipotent_ex_pr (ale _ iI)) => [[[fg ig] _] _].
  rewrite /f; split; fprops;aw.
apply: ext_map_prod_fs =>//.
move=> i iI; move: (equipotent_ex_pr (ale _ iI)) => [[ig sg] _ p4].
by rewrite /f -p4; apply: surjective_pr3.
Qed.

Lemma equipotent_setX a b a' b':
  a \Eq a' -> b \Eq b' -> (a \times b) \Eq (a' \times b').
Proof.
rewrite !equipotentC.
move=> [f bf] [g bg]; exists (ext_to_prodC f g).
apply: (bijective_ext_to_prod2C bf bg).
Qed.

Hint Resolve equipotent_setX equipotent_setXb: fprops.

commutativity asssociativity distributivity of product equipotency

Lemma product2A a b c:
  (a \times (b \times c)) \Eq ((a \times b) \times c).
Proof.
pose g z := J (J (P z) (P (Q z))) (Q (Q z)).
exists (Lf g (a \times (b \times c)) ((a \times b) \times c)).
split => //; aw.
rewrite /g; apply: lf_bijective.
    move=> d /setX_P [pa pb] /setX_P [pc pd pe].
    apply:setXp_i => //; apply:setXp_i => //.
  move=> u v /setX_P [pu Pu] /setX_P [pQu PQu QQu]
             /setX_P [pv Pv] /setX_P [pQv PQv QQv] eq.
  move:(pr1_def eq)(pr2_def eq)=> eq1 eq2.
  move:(pr1_def eq1)(pr2_def eq1)=> eq3 eq4.
  apply: pair_exten=>//; apply: pair_exten =>//.
move => y /setX_P [py] /setX_P [pPy PP QP] Qc.
exists (J (P (P y)) (J (Q (P y)) (Q y))) => //.
  apply:setXp_i => //; apply:setXp_i => //.
by aw;rewrite pPy py.
Qed.

Lemma distrib_union_prod2: right_distributive product union2.
Proof.
move => a b c;set_extens x.
  move /setX_P => [pa pb] /setU2_P.
  by case => pc; apply /setU2_P; [left | right]; apply:setX_i.
case /setU2_P => /setX_P [pa pb pc]; apply/setX_i => //; fprops.
Qed.

Lemma distrib_inter_prod2: right_distributive product intersection2.
Proof.
move => a b c;set_extens x.
 by move/setX_P => [Px xa /setI2_P [pa pb]]; apply/setI2_P;split;apply/setX_P.
move /setI2_P => [] /setX_P [Px px qx1 /setX_P [_ _ qx2]].
apply/setX_P; split; fprops.
Qed.

Lemma equipotent_times_s1s1 a b c: (a *s1 b) \Eq (a *s1 c).
Proof. eqtrans a; eqsym; fprops. Qed.

Hint Resolve equipotent_times_s1s1: fprops.

Properties of disjoint sets

Lemma disjointU2_pr0 a b x y:
  disjoint x y -> disjoint (a \times x) (b \times y).
Proof.
move=> dxy; apply: disjoint_pr.
move=> u /setX_P [_ _ qx] /setX_P [_ _ qy].
apply: (nondisjoint qx qy dxy).
Qed.

Lemma disjointU2_pr1 x y:
  x <> y -> disjoint (singleton x) (singleton y).
Proof. by move=> xy;apply: disjoint_pr; move => u /set1_P -> /set1_P. Qed.

Lemma disjointU2_pr a b x y:
  x <> y -> disjoint (a *s1 x) (b *s1 y).
Proof. by move=> xy; apply: disjointU2_pr0; apply: disjointU2_pr1. Qed.

Hint Resolve disjointU2_pr: fprops.

Lemma equipotent_disjointU X Y:
  fgraphs_equipotent X Y ->
  mutually_disjoint X -> mutually_disjoint Y ->
  (unionb X) \Eq (unionb Y).
Proof.
move=> [dXY ale] mX mY.
pose g i := equipotent_ex (Vg X i) (Vg Y i).
set X' := (Lg (domain X) (Vg X)).
have pfX: partition_w_fam X' (unionb X).
   rewrite /X';split; fprops; bw.
     by red; bw; move => a b ax bx; bw; apply: mX.
   by rewrite (unionb_gr X).
pose h i := change_target_fun (g i) (unionb Y).
have fph: forall i, inc i (domain X')-> function_prop (h i)(Vg X' i) (unionb Y).
  rewrite /X'; bw; move=> i idx; bw.
  move: (equipotent_ex_pr (ale _ idx)) => [[[fg _] _] sg tg].
  red;rewrite /h/change_target_fun; aw;split => //.
  apply: function_pr; fprops.
    apply: (@sub_trans (target (g i))).
      apply: f_range_graph=>//.
    rewrite tg; move=> t tf; union_tac; ue.
  rewrite f_domain_graph //.
move:(extension_partition1 pfX fph).
set x := common_ext _ _ _;move=> [[fx sx tx] agx'].
have agx:forall i, inc i (domain X) -> agrees_on (Vg X i) x (h i).
   move: agx'; rewrite /X';bw => h1 i idx; move: (h1 _ idx); bw.
exists x; split => //.
split.
  split=>//.
  rewrite sx;move=> a b /setUb_P [i idX ai] /setUb_P [j jdX bj].
  have ->: Vf x a = Vf (g i) a.
    move:(agx _ idX) => [_ _ ha];rewrite (ha _ ai) /Vf /h/change_target_fun; aw.
  have ->: Vf x b = Vf (g j) b.
    move:(agx _ jdX) => [_ _ hb];rewrite (hb _ bj) /Vf /h/change_target_fun; aw.
  move: (equipotent_ex_pr (ale _ idX)) => [[[fg ig] _] sg tg].
  move: (equipotent_ex_pr (ale _ jdX)) => [[[fg' _] _] sg' tg'].
  have Wta: (inc (Vf (g i) a) (Vg Y i)) by rewrite -tg /g ; Wtac.
  have Wtb: (inc (Vf (g j) b) (Vg Y j)) by rewrite - tg' /g; Wtac.
  rewrite dXY in idX jdX.
  case: (mY _ _ idX jdX) => eq.
     rewrite -eq in bj |- * ; apply: ig; ue.
  move=> eq'; rewrite -eq' in Wtb.
  by red in eq;empty_tac1 (Vf (g i) a ).
split => //.
rewrite tx=> y /setUb_P; rewrite -dXY; move=> [i idX yV].
move: (equipotent_ex_pr (ale _ idX)) => [[_ sg] srg tg].
rewrite -tg in yV; move: ((proj2 sg) _ yV) => [z zsg Wg].
move: (agx _ idX)=> [s1 s2 v].
exists z; first by apply: s1; ue.
rewrite srg in zsg; rewrite v// -Wg /Vf /h /change_target_fun; aw.
Qed.

Lemma equipotent_disjointU1 X Y:
  fgraphs_equipotent X Y ->
  (disjointU X) \Eq (disjointU Y).
Proof.
move=> [pc pd].
apply: equipotent_disjointU; rewrite /fgraphs_equipotent; fprops.
split; rewrite/disjointU_fam -? dXY; fprops; bw.
move=> i idy; bw; fprops; try ue.
eqtrans (Vg X i); [by eqsym; fprops | eqtrans (Vg Y i)].
Qed.

Lemma union2Lv a b: a \cup b = unionb (variantLc a b).
Proof.
rewrite/unionb; bw; rewrite setUf2f.
by rewrite variant_V_ca variant_V_cb.
Qed.

Lemma disjointLv a b: disjoint a b ->
   mutually_disjoint (variantLc a b).
Proof.
move=> db i j; bw => id1 jd; try_lvariant id1; try_lvariant jd; fprops.
by right;apply:disjoint_S.
Qed.

Lemma equipotent_disjointU2 a b a' b':
  disjoint a b -> disjoint a' b' -> a \Eq a' -> b \Eq b' ->
  (a \cup b) \Eq (a' \cup b').
Proof.
move=> dab dab' eqq' ebb'.
rewrite ! union2Lv; apply:equipotent_disjointU; try apply: disjointLv =>//.
red;bw; split => // i ind; try_lvariant ind.
Qed.

Definition doubleton_fam f a b :=
  exists x y, [/\ x<>y, fgraph f, domain f = doubleton x y,
    Vg f x = a & Vg f y = b].

Lemma doubleton_fam_canon f:
  doubleton_fam (Lg C2 f) (f C0) (f C1).
Proof. exists C0; exists C1; split => //;bw; fprops. Qed.

Lemma two_terms_bij a b f: doubleton_fam f a b ->
  let F := (variantLc a b) in
  exists g, [/\ bijection g, target g = domain F &
    f = F \cf (graph g)].
Proof.
move => [x [y [xy fgf df fx fy]]] F.
move: (set2_equipotent1 xy) => [g [[bg sg tg] ga gb]].
rewrite /F;exists g;split;fprops; first by aw; bw.
move: (f_domain_graph (proj1 (proj1 bg))); rewrite sg => dg.
apply: fgraph_exten; fprops.
  by rewrite /composef; bw; rewrite dg.
rewrite /composef dg.
rewrite df => z; case /set2_P => ->; rewrite /composef; bw; fprops.
rewrite -/(Vf g x) ga; bw.
rewrite -/(Vf g y) gb; bw.
Qed.

EIII-3-2 Order relation between cardinals


Definition equipotent_to_subset x y:= exists2 z, sub z y & x \Eq z.

Lemma eq_subset_ex_injP x y:
  equipotent_to_subset x y <->
  (exists f, injection_prop f x y).
Proof.
rewrite/equipotent_to_subset; split.
  move=> [z zy [f [[injf srj] sf tf]]].
  exists ((canonical_injection z y) \co f).
  hnf; rewrite /canonical_injection; aw; split => //.
  by apply: inj_compose1=>//; [apply: ci_fi=>// | aw].
move=> [f [injf srf tgf]].
exists (image_of_fun f).
  rewrite -tgf; apply: fun_image_Starget; fct_tac.
exists (restriction_to_image f).
hnf;rewrite /restriction_to_image /restriction2; aw.
split => //;by apply: restriction_to_image_fb.
Qed.

Lemma eq_subset_pr2 a b a' b':
   a \Eq a' -> b \Eq b' ->
   equipotent_to_subset a b -> equipotent_to_subset a' b'.
Proof.
move=> eq1 [f [[injf _] sf tf]].
have [g [[injg _] sg tg]]: a' \Eq a by eqsym.
move/eq_subset_ex_injP => [h [ih sh th]].
apply /eq_subset_ex_injP; exists ((f \co h) \co g); split => //; aw.
have ch: f \coP h by split => // ;try fct_tac; ue.
apply: compose_fi => //.
  apply: compose_fi => //.
split => //; try fct_tac; aw; ue.
Qed.

Lemma eq_subset_cardP x y:
  equipotent_to_subset x y <-> equipotent_to_subset (cardinal x) (cardinal y).
Proof.
move: (cardinal_pr x)(cardinal_pr y) => h1 h2.
split => aux.
  apply: (eq_subset_pr2 (equipotentS h1)(equipotentS h2) aux).
apply: (eq_subset_pr2 h1 h2 aux).
Qed.

Definition cardinal_le x y :=
  [/\ cardinalp x, cardinalp y & sub x y].
Definition cardinal_lt a b := cardinal_le a b /\ a <> b.

Notation "x <=c y" := (cardinal_le x y) (at level 60).
Notation "x <c y" := (cardinal_lt x y) (at level 60).

Lemma ordinal_cardinal_le x y:
  x <=c y -> x <=o y.
Proof. by move=> [[ox _] [oy _] le]. Qed.

Lemma cardinal_le_aux1 x y:
  x <=c y -> equipotent_to_subset x y.
Proof. move => [_ _ h]; exists x; fprops. Qed.

Lemma cardinal_le_aux2P x y: cardinalp x -> cardinalp y ->
  (equipotent_to_subset x y <-> x <=c y).
Proof.
move=> cx cy.
split; last by apply: cardinal_le_aux1.
move => [z zy ezx]; split => //.
move: (OS_cardinal cx)(OS_cardinal cy) => ox oy.
case: (ord_le_to_si ox oy) => // yx.
suff: (y \Eq z).
  move=> eyz.
  have : x \Eq y by eqtrans z; eqsym.
  move /card_eqP.
  rewrite (card_card cx) (card_card cy); move => -> //.
move: ezx => [f [[[f0 f1] _] f2 f3]].
have syx: (sub y x) by apply: (ordinal_transitive ox yx).
have p1: forall t, inc t y -> inc (Vf f t) z.
  by move=> t ty; rewrite -f3; Wtac;rewrite f2; apply: syx.
have p2: (forall u v, inc u y -> inc v y -> Vf f u = Vf f v -> u = v).
  by move=> u v ue ve; apply: f1; rewrite f2; apply: syx.
apply: (Cantor_Bernstein1 zy p1 p2).
Qed.

Lemma eq_subset_cardP1 x y:
  equipotent_to_subset x y <-> (cardinal x) <=c (cardinal y).
Proof.
apply: (iff_trans (eq_subset_cardP x y)).
split; first by move/cardinal_le_aux2P; apply; fprops.
apply: cardinal_le_aux1.
Qed.

Lemma incr_fun_morph f: injection f ->
  (cardinal (source f)) <=c (cardinal (target f)).
Proof.
move=> injf; apply /eq_subset_cardP1.
by apply/eq_subset_ex_injP; exists f.
Qed.

Lemma sub_smaller a b:
  sub a b -> (cardinal a) <=c (cardinal b).
Proof. move=> ab; apply /eq_subset_cardP1; exists a; fprops. Qed.

Lemma card_leR x: cardinalp x -> x <=c x.
Proof. by move=> cx;split. Qed.

Hint Resolve card_leR: fprops.

Lemma card_leT a b c:
  a <=c b -> b <=c c -> a <=c c.
Proof.
rewrite/cardinal_le.
by move=> [ca cb eab] [_ cc ebc]; split => //; apply: sub_trans eab ebc.
Qed.

Lemma card_leA x y:
  x <=c y -> y <=c x -> x = y.
Proof.
by move => [ca cb eab] [_ cc ebc]; apply: extensionality.
Qed.

Theorem cardinal_le_wor: worder_r cardinal_le.
Proof.
split => //.
  split => //.
  move=> a b c;apply: card_leT.
  move=> a b; apply: card_leA.
  move=> x y [cx cy _]; split; fprops.
move=> x xa [a ax].
have xc: cardinal_set x by move=> b bx; move: (xa _ bx)=> [ok _].
have xb: ordinal_set x by move=> b bx; move: (xa _ bx)=> [[ok _] _].
move: (least_ordinal1 (p:= fun w => (inc w x)) (xb _ ax) ax).
set y := least_ordinal (fun w => inc w x) a; move => [p1 p2 p3].
exists y; red; rewrite graph_on_sr //.
split => //; move=> u ux; apply graph_on_P1;split;fprops; split; fprops.
Qed.

The order on cardinals

Lemma not_card_le_lt a b: a <=c b -> b <c a -> False.
Proof. by move=> ab [ba nba]; case: nba; apply: card_leA.
Qed.

Lemma card_lt_leT a b c:
  a <c b -> b <=c c -> a <c c.
Proof.
move=> [ab nab] bc; split.
  apply: (card_leT ab bc).
by dneg ac; rewrite -ac in bc; apply: card_leA.
Qed.

Lemma card_le_ltT a b c:
  a <=c b -> b <c c -> a <c c.
Proof.
move=> ab [bc nbc]; split.
  apply: (card_leT ab bc).
by dneg ca; rewrite ca in ab; apply: card_leA.
Qed.

Lemma card_ltleA a b: a <c b -> ~(b <=c a).
Proof. move => h1 h2; exact: (not_card_le_lt h2 h1). Qed.

Lemma card_leltA a b: a <=c b -> ~(b <c a).
Proof. move => h1 h2; exact: (not_card_le_lt h1 h2). Qed.

Lemma card_lt_ltT a b c: a <c b -> b <c c -> a <c c.
Proof. move => h1 [h2 _]; exact: (card_lt_leT h1 h2). Qed.

Ltac co_tac := match goal with
  | Ha: ?a <=c ?b, Hb: ?b <=c ?c |- ?a <=c ?c
     => apply: (card_leT Ha Hb)
  | Ha: ?a <c ?b, Hb: ?b <=c ?c |- ?a <c ?c
     => apply: (card_lt_leT Ha Hb)
  | Ha:?a <=c ?b, Hb: ?b <c ?c |- ?a <c ?c
     => apply: (card_le_ltT Ha Hb)
  | Ha: ?a <c ?b, Hb: ?b <c ?c |- ?a <c ?c
     => induction Ha; co_tac
  | Ha: ?a <=c ?b, Hb: ?b <c ?a |- _
    => case: (not_card_le_lt Ha Hb)
  | Ha: ?x <=c ?y, Hb: ?y <=c ?x |- _
   => solve [ rewrite (card_leA Ha Hb) ; fprops ]
  | Ha: ?a <=c _ |- cardinalp ?a => exact (proj31 Ha)
  | Ha: _ <=c ?a |- cardinalp ?a => exact (proj32 Ha)
  | Ha: ?a <c _ |- cardinalp ?a => exact (proj31_1 Ha)
  | Ha: _ <c ?a |- cardinalp ?a => exact (proj32_1 Ha)
  | Ha: ?a <c ?b |- ?a <=c ?b => by move: Ha => []
end.

Lemma wordering_cardinal_le_pr x:
  cardinal_set x ->
  (worder_on (graph_on cardinal_le x) x).
Proof.
move=> alc; apply: (wordering_pr cardinal_le_wor).
move=> a ax; move: (alc _ ax); fprops.
Qed.

Lemma card_le_to_ell a b:
  cardinalp a -> cardinalp b ->
  [\/ a = b, a <c b | b <c a].
Proof.
move=> ca cb.
rewrite /cardinal_lt /cardinal_le.
move: (ca)(cb) => [oa _] [ob _].
case: (ordinal_trichotomy oa ob) => h.
- by constructor 2; move: (ordinal_sub2 ob h) => [p1 p2].
- by constructor 3; move: (ordinal_sub2 oa h) => [p1 p2].
- by constructor 1.
Qed.

Lemma card_le_to_el a b:
  cardinalp a -> cardinalp b ->
  a <=c b \/ b <c a.
Proof.
move=> ca cb; case: (card_le_to_ell ca cb).
  move=> ->; left; fprops.
 by move => [p1 _]; left.
by right.
Qed.

Lemma card_le_to_ee a b:
  cardinalp a -> cardinalp b ->
  a <=c b \/ b <=c a.
Proof.
move=> ca cb; case: (card_le_to_el ca cb); first by left.
by move =>[p1 _]; right.
Qed.

Lemma cardinal_ordinal_lt1 a x: cardinalp x -> inc a x ->
  cardinal a <c x.
Proof.
move => cx ax.
have ox: ordinalp x by apply: OS_cardinal.
move: (ordinal_hi ox ax) => oa.
have [_ h]: cardinalp (cardinal a) by fprops.
have aux: cardinal a \Eq a by fprops.
move: (h _ oa aux) => s1.
move: (ordinal_transitive ox ax) => sax.
split; first by split => //; fprops; apply: (sub_trans s1 sax).
move=> bad; rewrite bad in s1.
exact (ordinal_irreflexive oa (s1 _ ax)).
Qed.

Lemma ordinal_cardinal_le1 x y: x <=o y -> (cardinal x) <=c (cardinal y).
Proof.
move => [pa pb pc]; apply /eq_subset_cardP1; exists x; fprops.
Qed.

Lemma ordinal_cardinal_lt x y: x <c y -> x <o y.
Proof. by move=> [pa pb];split => //; apply: ordinal_cardinal_le. Qed.

Lemma ordinal_cardinal_le2P x y: cardinalp x -> ordinalp y ->
  ((y <o x) <-> (cardinal y <c x)).
Proof.
move=> cx oy; rewrite -{2} (card_card cx).
move: cx => [ox xp].
split; move => [p1 p2].
   move: (ordinal_cardinal_le1 p1) => p5; split => //; dneg p3.
   apply: ord_leA => //; split => //; apply: xp => //.
   by eqsym; move: p3; move/card_eqP.
case: (ord_le_to_el ox oy) => // p3.
move: (ordinal_cardinal_le1 p3)=> r1; case: p2; co_tac.
Qed.

Lemma ordinals_card_ltP y: cardinalp y ->
  forall x, inc x y <-> (ordinalp x /\ (cardinal x) <c y).
Proof.
move => cy x; move: (proj1 cy) => oy.
split.
  move /(ord_ltP oy) => xy; move: (proj31_1 xy) => ox;split => //.
  by apply /(ordinal_cardinal_le2P cy ox).
move => [ox].
by move /(ordinal_cardinal_le2P cy ox) /(ord_ltP oy).
Qed.

Lemma ordinal_cardinal_le3 x y:
   cardinalp x -> cardinalp y -> x <=o y -> x <=c y.
Proof.
move => cx cy h; move: (ordinal_cardinal_le1 h).
by rewrite (card_card cx) (card_card cy).
Qed.

Lemma ordinal_cardinal_lt3 x y:
   cardinalp x -> cardinalp y -> x <o y -> x <c y.
Proof. by move=> cx cy [le ne]; split => //; apply: ordinal_cardinal_le3. Qed.

Lemma finite_cP x: finite_c x <-> (cardinalp x /\ x <> succ x).
Proof.
split => [ fx | [cx xsx]].
  have cx: cardinalp x by fprops.
  split => //.
  move: fx => [p1 p2]; dneg h; apply /card_eqP.
  rewrite -/(succ x) -h card_card//.
split; first by apply: OS_cardinal.
dneg infx; red in infx; rewrite /succ -{1} (card_card cx).
by apply /card_eqP.
Qed.

Lemma infinite_cP x: infinite_c x <-> (cardinalp x /\ x = succ x).
Proof.
rewrite /infinite_c /succ/infinite_o.
split; move=> [cx].
  by rewrite -{4} (card_card cx); move /card_eqP=> aux.
by rewrite -{1} (card_card cx); move /card_eqP=> aux.
Qed.

Lemma finite_dichot x: cardinalp x -> finite_c x \/ infinite_c x.
Proof.
move=> cx; case: (equal_or_not x (succ x)) => h