# Theory of Sets : Ordinals

Copyright INRIA (2011-2013) Marelle Team (Jose Grimm).

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

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

Module Ordinals4.

## Epsilon ordinals

Definition ordinal_epsilon x := ordinalp x /\ omega0 ^o x = x.

Lemma ord_eps_p1 x: ordinalp x -> x <=o (omega0 ^o x).
Proof.
move=> ox.
move: (oprod_M1le ord_lt_0omega ox) (opow_Mspec2 ox ord_le_2omega) => ha hb.
ord_tac.
Qed.

Lemma ord_eps_p2 a b c (x := ((omega0 ^o a) *o b) +o c) :
ordinalp a -> \0o <o b -> ordinalp c ->
(a <=o x /\ (x = a -> [/\ c = \0o, b = \1o & ordinal_epsilon x])).
Proof.
move=> oa bp oc.
move: OS_omega => oo.
have ob: ordinalp b by ord_tac.
have op: ordinalp (omega0 ^o a) by fprops.
have ot: ordinalp ((omega0 ^o a) *o b) by fprops.
have ox: ordinalp x by rewrite /x;fprops.
move: (ord_eps_p1 oa) => le1.
move: (oprod_Mle1 op bp) => le2.
move: (osum_Mle0 ot oc) => le3.
move: (ord_leT le1 le2) => le4.
split; first by ord_tac.
move=> xa; rewrite xa; rewrite -/x in le3.
have pa: a = ((omega0 ^o a) *o b) by rewrite xa in le3; ord_tac.
have c0: c = \0c by apply: (osum_a_ab oa oc); rewrite -{2} xa /x -pa.
case: (ord_one_dichot bp) => b1.
by split => //; split => //; rewrite {2} pa b1 oprod1r.
move: (oprod_Meq1lt b1 (omega_pow_pos oa)); rewrite - pa => h; ord_tac.
Qed.

Lemma ord_eps_p3 x: ordinal_epsilon x -> omega0 <o x.
Proof.
move: ord_le_2omega (opowx1 OS_omega) => o2 o1 [ox oex].
move:(omega_pow_pos ox); rewrite oex => xp.
case: (ord_one_dichot xp) => xo.
by move: (proj2 (ord_lt_leT ord_lt_12 o2)); rewrite - o1 - xo oex.
by move/(opow_Meqltr o2 OS1 ox): xo; rewrite o1 oex.
Qed.

Lemma ord_eps_p4: iclosed_collection (ordinal_epsilon).
Proof.
by move: (iclosed_fixpoints (opow_normal ord_le_2omega)) => [].
Qed.

Definition epsilon_fct := the_least_fixedpoint_ge (ord_pow omega0).
Definition epsilon_fam := first_derivation (ord_pow omega0).

Lemma epsilon_fct_pr0 x: ordinalp x ->
least_fixedpoint_ge (ord_pow omega0) x (epsilon_fct x).
Proof. exact: (normal_ofs_fix (opow_normal ord_le_2omega)). Qed.

Lemma epsilon_fct_pr1 x: ordinalp x ->
ordinal_epsilon (epsilon_fct x).
Proof.
move => ox; move: (epsilon_fct_pr0 ox) => [pa pb _].
split => //; ord_tac.
Qed.

Lemma epsilon_fct_pr2 C (E:= succ_c C): infinite_c C ->
(forall x, inc x E -> inc (epsilon_fct x) E).
Proof.
move => iC.
apply:next_fix_point_small => //.
apply: opow_normal; apply: ord_le_2omega.
move:(succ_c_pr1 (proj1 iC)); rewrite -/E; move=> [pa pb pc].
move => x xe; apply:succ_c_pow => //.
by move:OS_omega => ha; apply: succ_c_leomega => //;ord_tac.
Qed.

Lemma epsilon_fct_pr3 (e:= epsilon_fct \1o ) :
ordinal_epsilon e /\
forall x, ordinal_epsilon x -> e <=o x.
Proof.
move: (epsilon_fct_pr0 OS1) => [pa pb pc]; split.
split => //; ord_tac.
move => x h; move: (ord_le_ltT (ozero_least OS_omega) (ord_eps_p3 h)) => x1.
move: h => [ox oex]; apply: pc => //; ord_tac1.
Qed.

Lemma epsilon_fam_pr0 x: ordinalp x ->
ordinal_epsilon (epsilon_fam x).
Proof.
move: (iclosed_fixpoints (opow_normal ord_le_2omega)) => [pa pb].
by move:(ordinals_col_p1 (proj1 pa) pb) => [na _ _ _ _]; move /na.
Qed.

Lemma epsilon_fam_pr1 y: ordinal_epsilon y ->
exists2 x, ordinalp x & y = epsilon_fam x.
Proof.
move: (iclosed_fixpoints (opow_normal ord_le_2omega)) => [pa pb].
move:(ordinals_col_p1 (proj1 pa) pb) => [_ na _ _ _];apply:na.
Qed.

Lemma epsilon_fam_pr2: epsilon_fam \0o = epsilon_fct \1o.
Proof.
apply:first_derivation_p2; first by apply:(opow_normal ord_le_2omega).
apply: omega_pow_nz; fprops.
Qed.

Lemma epsilon_fam_pr2': epsilon_fam \0o = epsilon_fct \0o.
Proof.
apply:first_derivation_p1; by apply:(opow_normal ord_le_2omega).
Qed.

Lemma epsilon_fam_pr2'': epsilon_fam \0o = epsilon_fct (succ_o omega0).
Proof.
rewrite epsilon_fam_pr2'; rewrite /epsilon_fct.
move:(opow_normal ord_le_2omega) => nf.
move: (normal_ofs_fix nf OS0) => [].
set u := the_least_fixedpoint_ge _ _; move => [_ sa _] sb sc.
move: (normal_ofs_fix nf (OS_succ OS_omega)) => [].
set v := the_least_fixedpoint_ge _ _; move => [_ sa' _] sb' sc'.
apply: ord_leA; first by apply: sc => //; ord_tac1.
apply: sc' => //; apply /ord_succ_ltP; exact : (ord_eps_p3 (conj sa sb)).
Qed.

Lemma epsilon_fam_pr3 x y: ordinalp x ->
epsilon_fam x <o y -> y <=o epsilon_fam (succ_o x) ->
epsilon_fct y = epsilon_fam (succ_o x).
Proof.
move => ox.
move: (iclosed_fixpoints (opow_normal ord_le_2omega)) => [pa pb].
move: (iclosed_col_fs pa pb ox).
rewrite /epsilon_fam/first_derivation.
set fx := (ordinalsf _ x); set fy := (ordinalsf _ (succ_o x)).
move => [fxy ex [ofy ey] etc] l1 l2.
move: (epsilon_fct_pr0 (proj31 l2)); set z := (epsilon_fct y).
move => [sa sb sc]. apply:ord_leA; first by apply: sc.
apply: etc; [ split => //;ord_tac | ord_tac ].
Qed.

Lemma epsilon_fam_pr4 x: ordinalp x ->
epsilon_fam (succ_o x) = epsilon_fct (succ_o (epsilon_fam x)).
Proof.
apply: first_derivation_p3;apply: (opow_normal ord_le_2omega).
Qed.

Lemma epsilon_fam_pr5: normal_ofs epsilon_fam.
Proof.
move: (iclosed_fixpoints (opow_normal ord_le_2omega)) => [pa pb].
exact: (ordinals_col_p2 pa pb).
Qed.

Lemma epsilon_fam_pr6 C (E := succ_c C)
(F:= Zo E ordinal_epsilon) : infinite_c C ->
order_isomorphism (Lf epsilon_fam E F) (ordinal_o E) (graph_on ordinal_le F).
Proof.
move => ic.
have aux:forall x,inc x (succ_c C) -> inc (omega0 ^o x) (succ_c C).
move => x xe; apply:succ_c_pow => //.
by move:OS_omega => ha; apply: succ_c_leomega => //;ord_tac.
move: (first_derivation_p4 ic (opow_normal ord_le_2omega) aux).
have -> //: (Zo E (fun z => omega0 ^o z = z)) = F.
apply: Zo_exten1 => x xE; split; [move => h; split => // | by move => []].
by move/(succ_cP (proj1 ic)):xE => [].
Qed.

Lemma epsilon_fam_pr7 C (E := succ_c C)
(F:= Zo E ordinal_epsilon) : infinite_c C -> cardinal E = cardinal F.
Proof.
move /epsilon_fam_pr6; rewrite -/F -/E; move => [_ _ [bf _ _] _].
apply /card_eqP; exists (Lf epsilon_fam E F); split => //; aw.
Qed.

Lemma countable_epsilon x: ordinalp x ->
(countable_ordinal x <-> countable_ordinal (epsilon_fam x)).
Proof.
move: omega_infinitec aleph_oneP => h T.
move: (epsilon_fam_pr6 h) => [_ _ [bf _ _] _].
set E := (succ_c omega0) in T bf.
set f := (Lf epsilon_fam E (Zo E ordinal_epsilon)).
have ff: function f by move: bf => [[]].
have sf: source f = E by rewrite /f; aw.
have tf: target f = (Zo E ordinal_epsilon) by rewrite /f; aw.
have H: lf_axiom epsilon_fam E (Zo E ordinal_epsilon).
move => s sE; move: (sE); rewrite - {1} sf => / (Vf_target ff).
by rewrite tf /f /Lf /Vf /graph pr1_pair LVg_E.
move => ox; split; first by move /T /H /Zo_S/T.
move /T => h1; apply /T.
have wa: inc (epsilon_fam x) (target f).
by rewrite tf; apply /Zo_P; split => //; apply: epsilon_fam_pr0.
move: (proj2 (proj2 bf) _ wa); aw; move => [a ae]; aw=> eq.
move/(succ_cP (proj1 h)):(ae) => [oa _].
move: epsilon_fam_pr5 => [ii _].
by case:(ord_le_to_ell ox oa); first (by move => ->); move /ii =>[]; rewrite eq.
Qed.

Definition Cantor_Omega := aleph_one -s omega0.

Lemma Cantor_omega_pr x:
inc x Cantor_Omega <-> (countable_ordinal x /\ omega0 <=o x).
Proof.
split.
move /setC_P => [/aleph_oneP pa pb]; split => //.
by case: (ord_le_to_el OS_omega (proj1 pa)) => // /ord_ltP0 [_ _].
move => [pa pb]; apply/setC_P; split; first by apply /aleph_oneP.
by move => xo; move: (proj33 pb _ xo)(ordinal_irreflexive (proj32 pb)).
Qed.

Lemma Cantor_omega_pr2: cardinal Cantor_Omega = aleph_one.
Proof.
move: omega_infinitec => h.
move: (succ_c_pr1 (proj1 h)); rewrite - /aleph_one; move => [pa pb pc].
move:(ordinal_cardinal_lt pb) => pd.
by move:(cardinal_indecomposable1 (ge_infinite_infinite h (proj1 pb)) pd) => [].
Qed.

Lemma critical_productP:
let CP := critical_ordinal \1o ord_prod2 in
let p1 := fun y => (exists2 n, ordinalp n & y = omega0 ^o (omega0 ^o n)) in
let p2 := fun y => [/\ infinite_o y, ordinalp y &
(forall z, \1o <o z -> z <=o y ->
exists t, [/\ ordinalp t, ord_indecomposable t & y = z ^o t])] in
forall y, (p1 y <-> p2 y) /\ (CP y <-> p1 y).
Proof.
move=> CP p1 p2.
move: ord_lt_1omega => lt1o.
move: OS_omega OS1=> oo o1.
move: ord_lt_01 => l01.
have auxP: forall y, ordinalp y -> (infinite_o y <-> (omega0 <=o y)).
move=> y oy; split; first by move/(omega_P1 oy) => h; split => //.
by move => [_ _ ] /(omega_P1 oy).
have p21: forall y, p2 y -> p1 y.
move=> y [iy oy yp]; move: iy => /(auxP _ oy) iy.
move: (yp _ lt1o iy) => [t [ot oit yv]].
move: (indecomp_prop3 oit) => [n on tb]; exists n => //;ue.
have p02: forall y, CP y -> p2 y.
move=> y [pa pb pc pd]; split => //.
move=> z z1 lezy; case: (equal_or_not z y) => zy.
exists \1o; rewrite zy (opowx1 pa); split => //; apply: indecomp_one.
have ltzy: z <o y by split.
move: (ord_le_ltT (proj1 (ord_lt_01)) pc) => y1.
have z2: \2o <=o z by rewrite - succ_o_one ; apply /ord_succ_ltP.
have oz: ordinalp z by ord_tac.
move: (ord_ext_div_exists z2 y1)
=> [a [b [c [oa ob oc [bv ltc ltv bnz]]]]].
set x1:= (z ^o a) *o b.
have le1: (z ^o a) <=o x1 by rewrite /x1; apply: oprod_Mle1; fprops.
have cx1: c <o x1 by ord_tac.
have co: \0o <=o c by apply: ozero_least.
have za1: \1o <=o (z ^o a) by apply /ord_ge1P; ord_tac.
have le2: \1o <=o x1 by ord_tac.
have ox1: ordinalp x1 by ord_tac.
have oza: ordinalp (z ^o a) by ord_tac.
case: (equal_or_not x1 y) => yx1; last first.
have ltx1y: x1 <o y by split => //; rewrite bv; apply: osum_Mle0.
move: (pd _ le2 ltx1y).
move: (ord_rev_pred y1); set u := (y -o \1o); move => [ou yv].
rewrite {1} yv bv -/x1 (osum_prodD OS1 ou ox1) (oprod1r ox1).
move=> aux1; move: (osum2_simpl (OS_prod2 ox1 ou) oc ox1 aux1) => e1.
case: (ord_zero_dichot ou) => uz.
by move: pc; rewrite yv uz (osum0r OS1); case.
move: (oprod_Mle1 ox1 uz); rewrite e1 => le3; ord_tac.
case: (equal_or_not (z ^o a) y) => zay; last first.
have lt1: (z ^o a) <o y by split=> //; rewrite - yx1.
move: (pd _ za1 lt1); rewrite -{2} yx1 /x1 => aux1.
have zaz: \0o <o z ^o a by ord_tac1.
move: (oprod2_simpl pa ob zaz aux1).
move=> aux2; rewrite - aux2 in ltv; ord_tac.
rewrite - zay; exists a;split => //.
case: (ord_zero_dichot oa) => az.
by move: pc=> [_ xx]; case: xx;rewrite - zay az opowx0.
apply /indecompP => // d da.
have od: ordinalp d by ord_tac.
have znz: \0o <o z by exact: (ord_lt_leT bnz (proj1 ltv)).
have ad1: \1o <=o (z ^o d) by apply /ord_ge1P;apply: opow_pos.
move: (opow_Meqlt z2 da); rewrite zay => p4.
move: (pd _ ad1 p4); rewrite - zay - opow_sum => //.
apply: opow_regular => //; fprops.
suff p10: forall y, p1 y -> CP y.
move=> y; split; split => h.
- by apply:p02; apply: p10.
- by apply: p21.
- by apply: p21; apply: p02.
- by apply:p10.
move=> y [n on yv].
have yif: omega0 <=o y.
rewrite yv - {1} (opowx1 OS_omega); apply: opow_Momega_le.
apply: (ord_ge1 (OS_pow oo on) (omega_pow_nz on)).
split; [ ue | by apply /(auxP _ (proj32 yif)) | ord_tac | ].
by rewrite yv => x x1 x2; exact: (oprod_crit_aux on x1 x2).
Qed.

Lemma ord_epsilon_p9 x a: ordinal_epsilon x -> a <o x->
[/\ a +o x = x,
(\1o <=o a -> a *o x = x) &
(\2o <=o a -> a ^o x = x) ].
Proof.
move=> oex lax.
move: (ord_eps_p3 oex) => oox.
move: oex => [ox xx].
have pa: forall n, \1o <=o n -> n <o x -> n *o x = x.
move: (critical_productP x) => [_ pb].
have: (exists2 n, ordinalp n & x = omega0 ^o (omega0 ^o n)).
by exists x => //;rewrite xx xx.
move /pb => [_ _ _ pd] //.
split.
by apply: indecomp_prop1 lax; rewrite -xx; apply: indecomp_prop4.
by move=> a1;apply: pa a1 lax.
move=> a2.
move: OS_omega => oo.
have oa: ordinalp a by ord_tac.
move: ord_lt_1omega => [lt1o _].
move: (pa _ lt1o oox) => oxx.
rewrite - {1} oxx (opow_prod oa oo ox).
case: (ord_le_to_el oo oa) => coa; last first.
by rewrite (opow_int_omega a2 coa).
case: (ord_zero_dichot oa) => ap.
move:ord_lt_02; rewrite - ap => bad1;ord_tac.
move:(the_CNF_p0 oa) => [/CNFB_ax_simp [mB ax] xv].
move: (the_CNF_p2 ap); set n:= cpred _; move => [nB nv].
rewrite nv in ax.
case (ord_zero_dichot (OS_the_CNF_degree oa)) => bz.
move: (proj2 (the_CNF_p4 ap)); rewrite bz.
rewrite succ_o_zero (opowx1 OS_omega) => bad1; ord_tac.
rewrite - xx in lax; move: (the_CNF_p6 ox ap lax) => h2.
move: (CNF_pow_pr3 ax bz nB); rewrite - nv -/(CNFBv _) xv => hh.
move: bz => [[_ oq _] qnz].
have lt1q: \1o <=o (the_CNF_degree a) by apply: ord_ge1; fprops.
move: (opow_prod oo (OS_prod2 oq oo) ox).
by rewrite -(oprodA oq oo ox) oxx - hh (pa _ lt1q h2) xx => <-.
Qed.

Lemma ord_epsilon_p10 x:
ordinal_epsilon x -> critical_ordinal \2o ord_pow x.
Proof.
move=> oex;move: (oex) => [ox _]; move: (ord_eps_p3 oex) => xo.
split => //.
apply /(omega_P1 ox); exact (proj33 (proj1 xo)).
move: ord_lt_2omega => h; ord_tac.
move=> a a2 ax; move: (ord_epsilon_p9 oex ax) => [_ _ p]; apply: (p a2).
Qed.

Lemma ord_epsilon_p11 x: ordinalp x -> (\2o ^o x = x) ->
x = omega0 \/ ordinal_epsilon x.
Proof.
move=> ox hx.
have H:=(opowx1 OS_omega).
move: (odivision_exists1 ox ord_lt_0omega)
=> [q [r [oq or av bv]]].
have le22: \2o <=o \2o by apply: ord_leR; fprops.
have oo:= OS_omega.
case: (equal_or_not r \0o) => rnz; last first.
have rB: inc r Bnat by apply /olt_omegaP.
move: (cpred_pr rB rnz) => [pb pv].
have ooq: ordinalp (omega0 *o q) by fprops.
have fp: finite_c (cpred r) by apply /BnatP.
move: pb => /olt_omegaP pb.
have op: ordinalp (cpred r) by ord_tac.
move: av; rewrite pv (succ_of_finite fp) - (osum2_succ ooq op).
set v := (omega0 *o q) +o cpred r => xs.
case: (equal_or_not v \0o) => vz.
move: hx; rewrite xs vz succ_o_zero (opowx1 OS2) => e12.
by move: ord_lt_12 => [_ ]; rewrite e12.
have ov: ordinalp v by rewrite /v; fprops.
have o2v: ordinalp (\2o ^o v) by fprops.
move: hx; rewrite xs (opow_succ OS2 ov) (ord_double o2v) => h.
case: (equal_or_not \1o v) => v1.
move: h; rewrite -v1 (opowx1 OS2) succ_o_one => h2.
by move: (osum_a_ab OS2 OS2 h2) ord_lt_02 => h3 [_]; rewrite - h3.
have lt1: \1o <o v by split=> //; apply: ord_ge1.
move: (opow_Mspec le22 ov) => le1.
move: (osum_Mlele le1 le1); rewrite h - (ord_succ_pr ov).
move: (osum_Meqlt lt1 ov) => pc pd; ord_tac.
move: av; rewrite rnz (osum0r); last by fprops.
move => xq; case: (ord_zero_dichot oq) => qz.
move: hx; rewrite xq qz oprod0r opowx0 => h1.
by symmetry in h1; move: ord_lt_01 => [_] h2.
case: (equal_or_not \1o q) => qo.
by left;rewrite xq -qo (oprod1r); fprops.
right.
have o2:= ord_lt_2omega.
move: hx; rewrite xq (opow_prod OS2 oo oq) (opow_int_omega le22 o2).
move: (ord_rev_pred qz); set y:= (q -o \1o); move => [yo yv].
rewrite yv (opow_sum oo OS1 yo) H => pa.
have ooy: ordinalp (omega0 ^o y) by fprops.
have o1y: ordinalp (\1o +o y) by rewrite - yv.
have onz: omega0 <> \0o by apply: omega_nz.
move: (oprod2_simpl ooy o1y ord_lt_0omega pa).
move: (opow_Mspec ord_le_2omega yo) => pc res1.
symmetry in res1.
case: (indecomp_pr OS1 yo (indecomp_prop4 yo) res1) => eq1.
by move: qo; rewrite yv res1 -eq1.
by rewrite res1 - {1} [omega0] H - (opow_sum oo OS1 yo) res1 -eq1 -eq1.
Qed.

Lemma ord_epsilon_p12 x: ordinalp x -> (\2o ^o x = x) ->
critical_ordinal \2o ord_pow x.
Proof.
move => ox ex; case: (ord_epsilon_p11 ox ex); last by apply: ord_epsilon_p10.
move: ord_lt_2omega => o2.
move => ->; split => //.
fprops.
apply: omega_infinite.
by move=> a a2 au; apply: opow_int_omega.
Qed.

Lemma ord_epsilon_p13 a x: ordinalp a -> ordinalp x -> (a ^o x = x) ->
( (a <o omega0 -> ((a = \1o /\ x = \1o) \/ (\2o ^o x = x)))
/\ (omega0 <=o a -> (ordinal_epsilon x /\ a <o x))).
Proof.
move => oa ox h.
have pa: \2o <=o a -> \2o ^o x = x.
move => a2; apply: ord_leA.
by move: (opow_Mleeq card2_nz a2 ox); rewrite h.
by move: (opow_Mspec (ord_leR OS2) ox).
case: (equal_or_not x \0o) => xnz.
move: ord_lt_01 => [_].
by move: h; rewrite xnz opowx0 => ->.
split => ao.
case: (ord2_trichotomy oa) => az.
- by move: h; rewrite az opow0x => h0; case: xnz.
- by left;split => //; rewrite -h az opow1x.
- by right; apply: pa.
move: (ord_leT (ord_le_2omega) ao) => a2.
move: (pa a2) => h1.
have x2 : \1o <o x.
split; first by apply:ord_ge1.
move => x1; move: h1; rewrite - x1 (opowx1 OS2) => h1.
by move: ord_lt_12; rewrite h1; case.
move: (opow_Meqlt a2 x2); rewrite (opowx1 oa) h => ax.
move: (ord_le_ltT ao ax) => [_ xo].
split; last by exact.
case:(ord_epsilon_p11 ox h1); [ by move => xno; case: xo | exact].
Qed.

Lemma pow_fix_enumeration1 a: \2o <=o a -> a <o omega0 ->
forall x, ordinalp x -> first_derivation (ord_pow a) x =
Yo (x = \0o) omega0 (epsilon_fam (x -o \1o)).
Proof.
move => age2 ao.
move: (opow_normal age2)=> npa.
move: (opow_normal ord_le_2omega)=> npb.
move: (iclosed_fixpoints npa) => [pa pb].
move:(ordinals_col_p2 pa pb) => na.
have oa:ordinalp a by ord_tac.
move: OS_omega => oo.
have aux: forall x, ordinalp x -> a ^o x = x -> x= omega0 \/ ordinal_epsilon x.
move => x ox h; apply: (ord_epsilon_p11 ox).
move: (ord_epsilon_p13 oa ox h) => [h1 _]; case: (h1 ao); last by exact.
move => [a1 _]; rewrite a1 in age2; move: ord_lt_12=> t; ord_tac.
have aux1 : forall x, ordinalp x -> a ^o x = x -> omega0 <=o x.
move => x ox xv; case: (aux _ ox xv); first by move => ->; ord_tac.
by move /ord_eps_p3 => [].
have aux2: forall x, ordinalp x -> omega0 ^o x = x -> a ^o x = x.
move => x ox oox; move: (conj ox oox) => xox.
move: (ord_lt_leT ao (proj1 (ord_eps_p3 xox))) => ax.
by move: (ord_epsilon_p9 xox ax) => [_ _]; apply.
move: (first_derivation_p0 npa) => npc.
have sd0:(first_derivation [eta ord_pow a] \0o) = omega0.
rewrite (first_derivation_p1 npa).
move: (normal_ofs_fix npa OS0) => [sa sb sc]; apply: ord_leA.
apply: sc; [ord_tac1 | by apply: opow_int_omega ].
apply: (aux1 _ (proj32 sa) sb).
apply:(normal_ofs_uniqueness (p:= fun z => (epsilon_fct (succ_o z)))).
- exact: npc.
- have aa: forall x,ordinalp x -> omega0 <o epsilon_fam x.
by move => x /epsilon_fam_pr0 /ord_eps_p3.
move:epsilon_fam_pr5 => [sa sb].
split.
move => u v uv /=.
case: (equal_or_not v \0o) => vnz; first by case: (@ord_lt0 u); ue.
Ytac0;Ytac uz; first by apply: aa;apply: (OS_diff OS1 (proj32_1 uv)).
apply: sa; apply:oprec_Mlt => //; move:(proj31_1 uv)=> ou;ord_tac1.
move => x lx; move: (limit_nz lx) => xnz; Ytac0.
move: (lx) => [ox zix lxx].
rewrite (odiff_1inf (omega_limit2 lx)) (sb _ lx).
have oe: forall z, inc z x -> ordinalp (epsilon_fam (z -o \1o)).
move=> z /(ordinal_hi ox) h;apply: (ofs_sincr sa); apply: (OS_diff OS1 h).
apply: ord_sup_1cofinal; first split.
* move => s /funI_P [z zx ->]; apply /funI_P.
have oz: ordinalp z by ord_tac.
case: (ord_le_to_el OS_omega oz) => czo.
exists z => //; rewrite (odiff_1inf czo); Ytac zz; last by exact.
move:ord_lt_0omega; rewrite - zz => h; ord_tac.
exists (succ_o z); first by apply: lxx.
move: (@succo_nz z) => zz; Ytac0; case: (ord_zero_dichot oz) => zz1.
by rewrite zz1 succ_o_zero (odiff_wrong (ord_leR OS1)).
by rewrite (oprec_nat2 zz1 czo) - (oprec_nat zz1 czo).
* move => s /funI_P [z zx ->]; Ytac zp.
exists (epsilon_fam \0o); first by apply/funI_P; ex_tac; ue.
exact: (proj1 (aa _ OS0)).
move: (ord_leR (oe _ zx)) => l1.
have ssx: inc (z -o \1o) x.
move: (odiff_Mle OS1 (ordinal_hi ox zx)) => h1.
move/(ord_ltP ox): zx => h;apply/(ord_ltP ox); ord_tac.
exists (epsilon_fam (z -o \1o)) => //; apply/funI_P; ex_tac.
* move => s /funI_P [z za ->]; Ytac zz;[ exact | by apply: oe].
- move => x ox; rewrite (first_derivation_p3 npa ox) /epsilon_fct.
move: (sincr_incr (proj1 npc) (ozero_least ox)); rewrite sd0.
move /ord_lt_succP; set t := succ_o _ => oot.
have ot: ordinalp t by ord_tac.
move: (normal_ofs_fix npa ot) (normal_ofs_fix npb ot).
move => [sa sb sc][sd se sf]; apply: ord_leA.
apply: (sc _ sd); apply: (aux2 _ (proj32 sd) se).
apply: (sf _ sa) ; case: (aux _ (proj32 sa) sb); last by move => [].
move => e1; rewrite e1 in sa; ord_tac.
- move => x ox; move: (@succo_nz x)=> snz; Ytac0.
case: (ord_le_to_el oo ox) => cox.
rewrite (odiff_1inf cox).
rewrite (odiff_1inf (ord_leT cox (proj1(ord_succ_lt ox)))).
Ytac xz; first by move: ord_lt_0omega; rewrite - xz => h1; ord_tac.
by apply:epsilon_fam_pr4.
case: (ord_zero_dichot ox) => xz.
Ytac0; rewrite xz succ_o_zero (odiff_wrong (ord_leR OS1)).
apply: epsilon_fam_pr2''.
move: (xz) => [_ xnz]; Ytac0; rewrite (oprec_nat2 xz cox).
by apply: epsilon_fam_pr4; apply: (OS_diff OS1 ox).
- Ytac0; exact sd0.
Qed.

Definition inverse_epsilon :=
ordinalr (fun x y => [/\ ordinal_epsilon x, ordinal_epsilon y & x <=o y]).

Lemma inverse_epsilon_pr x (y := inverse_epsilon x):
ordinal_epsilon x -> (ordinalp y /\ epsilon_fam y = x).
Proof. by apply:ordinalrsP => t []. Qed.

Lemma least_critical_pow a (b := inverse_epsilon (epsilon_fct (succ_o a))):
omega0 <=o a -> least_fixedpoint_ge (ord_pow a) \0o (epsilon_fam b).
Proof.
move => ooa.
move: (OS_succ (proj32 ooa)) => oa.
move:(epsilon_fct_pr1 oa) => oeea; move:(oeea) => [ooeea _].
move: (inverse_epsilon_pr oeea); rewrite -/b; move => [ob eb].
move:(epsilon_fct_pr0 oa); rewrite eb; move => [sa sb sc].
move: (ord_leT (ord_le_2omega) ooa) => a2.
split; first by ord_tac1.
have lt1: a <o epsilon_fct (succ_o a) by apply /ord_succ_ltP.
by move: (ord_epsilon_p9 oeea lt1)=> [_ _]; apply.
move => z zp h; move: (ord_epsilon_p13 (proj32 ooa) (proj32 zp) h) => [_ h1].
by move: (h1 ooa) => [[_ ta] tb]; apply: sc => //; apply /ord_succ_ltP.
Qed.

Lemma pow_fix_enumeration2 a (b := inverse_epsilon (epsilon_fct (succ_o a))):
omega0 <=o a ->
forall x, ordinalp x -> first_derivation (ord_pow a) x =
(epsilon_fam (b +o x)).
Proof.
move => ao.
move: (ord_leT ord_le_2omega ao) => age2.
move: (least_critical_pow ao); rewrite -/b; move => bp.
have oa: ordinalp a by ord_tac.
move:(inverse_epsilon_pr (epsilon_fct_pr1 (OS_succ oa))).
rewrite -/b; move => [ob eb].
move: (opow_normal age2)=> npa.
move: (opow_normal ord_le_2omega)=> npb.
move: (first_derivation_p0 npa) => npc.
move: (iclosed_fixpoints npa) => [pa pb].
move:(ordinals_col_p2 pa pb) => na.
move: OS_omega => oo.
have aux2: forall x, a <o x -> omega0 ^o x = x -> a ^o x = x.
move => x ax oox; move: (conj (proj32 (proj1 ax)) oox) => xox.
by move:(ord_epsilon_p9 xox ax) => [_ _]; apply.
have aux0: the_least_fixedpoint_ge [eta ord_pow a] \0o = epsilon_fam b.
move: (normal_ofs_fix npa OS0) => [sa sb sc].
move: bp => [sa' sb' sc'].
apply: ord_leA; [by apply:sc | by apply:sc'].
apply:(normal_ofs_uniqueness (p:= fun z => (epsilon_fct (succ_o z)))).
- exact: npc.
- exact: (normal_ofs_compose epsilon_fam_pr5 (osum_normal ob)).
- move => x ox; rewrite (first_derivation_p3 npa ox) /epsilon_fct.
have hh: \0o <=o x by ord_tac1.
move: (sincr_incr (proj1 npc) hh) => /ord_lt_succP.
rewrite (first_derivation_p1 npa) aux0.
set t := succ_o _; rewrite eb => sa1.
move:(epsilon_fct_pr0 (OS_succ oa)); move => [sa2 _ _].
move: (ord_le_ltT sa2 sa1) => [] /ord_succ_ltP lat _.
have ot: ordinalp t by ord_tac.
move: (normal_ofs_fix npa ot) (normal_ofs_fix npb ot).
move => [sa sb sc][sd se sf]; apply: ord_leA.
apply: (sc _ sd); apply: (aux2 _ _ se); by ord_tac.
apply: (sf _ sa).
move: (ord_epsilon_p13 oa (proj32 sa) sb) => [_ h1].
move: (h1 ao) => [[_ h2] _]; exact h2.
- move => x ox; rewrite - (osum2_succ ob ox); apply: epsilon_fam_pr4; fprops.
- rewrite (osum0r ob) - aux0 (first_derivation_p1 npa); reflexivity.
Qed.

Lemma all_der_sum_aux c (f:= ord_sum2 c)
(b:= fun x i => succ_c (card_max (omax c x) i)):
ordinalp c -> normal_ofs f /\ all_der_bound f b.
Proof.
move => oc; split; first by apply:osum_normal.
move => x i ox oi.
move: (OS_omax oc ox) => om.
move: (omax_p3 om oi); rewrite -/(card_max _ _) -/(b x i).
move => [sa sb sc].
have ec: exists2 C, infinite_c C & b x i = succ_c C.
by exists (card_max (omax c x) i).
move:(omax_p1 oc ox) => [sd se].
have ha: ordinalp (b x i) by exact: (proj1 (CS_succ_c (proj1 sa))).
move/(ord_ltP ha): sb => sf.
have pa: inc x (b x i) by apply /(ord_ltP ha); ord_tac.
have pb: inc c (b x i) by apply /(ord_ltP ha); ord_tac.
have pc: forall y, inc y (b x i) -> inc (c +o y) (b x i).
move => y ye;apply: succ_c_sum => //.
split => //.
Qed.

Lemma all_der_prod_aux c (f:= ord_prod2 c)
(b:= fun x i => succ_c (card_max (omax c x) i)):
\0o <o c -> normal_ofs f /\ all_der_bound f b.
Proof.
move => cp; split; first by apply:oprod_normal.
move => x i ox oi.
move: (proj32_1 cp) => oc.
move: (OS_omax oc ox) => om.
move: (omax_p3 om oi); rewrite -/(card_max _ _) -/(b x i).
move => [sa sb sc].
have ec: exists2 C, infinite_c C & b x i = succ_c C.
by exists (card_max (omax c x) i).
move:(omax_p1 oc ox) => [sd se].
have ha: ordinalp (b x i) by exact: (proj1 (CS_succ_c (proj1 sa))).
move/(ord_ltP ha): sb => sf.
have pa: inc x (b x i) by apply /(ord_ltP ha); ord_tac.
have pb: inc c (b x i) by apply /(ord_ltP ha); ord_tac.
have pc: forall y, inc y (b x i) -> inc (c *o y) (b x i).
move => y ye;apply: succ_c_prod => //.
split => //.
Qed.

Lemma all_der_pow_aux (f:= ord_pow omega0)
(b:= fun x i => succ_c (card_max x i)):
normal_ofs f /\ all_der_bound f b.
Proof.
split; first by exact: (opow_normal ord_le_2omega).
move => x i ox oi.
move: (omax_p3 ox oi) => [sa sb sc]; split => //.
by exists (card_max x i).
move => t tb; apply/succ_c_pow => //.
apply/(succ_cP (proj1 sa)); split; fprops.
apply:ordinal_cardinal_le1.
exact: (proj2 (omax_p1 (OS_omax ox oi) OS_omega)).
Qed.

Lemma all_der_sum c x i (f:= ord_sum2 c)
(b:= fun x i => succ_c (card_max (omax c x) i)):
ordinalp c -> ordinalp x -> ordinalp i ->
all_der f b x i = c *o omega0 ^o i +o x.
Proof.
move => oc ox oi0.
move: (all_der_sum_aux oc); rewrite -/b; move => [ha hb].
pose p i := forall x, ordinalp x -> all_der f b x i = c *o omega0 ^o i +o x.
move: x ox; rename i into i0.
apply: (least_ordinal2 (p := p)) oi0 => y oy etc.
case: (limit_ordinal_pr2 oy) => ly.
move => x ox; rewrite ly (all_der_p2 ha hb ox) opowx0 oprod1r//.
move:ly => [i oi si].
move => x ox.
have liy: i <o y by rewrite si;apply:ord_succ_lt.
have na: normal_ofs ((all_der f b)^~ i) by apply: all_der_p6.
move:(first_derivation_exten (etc _ liy) na) => eq1.
move:(all_der_p14 ha hb oi ox); rewrite - si => <- /=.
have oo1:= (OS_pow OS_omega oi).
have oo:=(OS_prod2 oc oo1).
rewrite (eq1 x ox) (add_fix_enumeration oo ox) si (opow_succ OS_omega oi).
by rewrite (oprodA oc oo1 OS_omega).
have nf:= (all_der_p6 ha hb oy).
have ooy := (OS_pow OS_omega oy).
have ov := OS_prod2 oc ooy.
have ng:= (osum_normal ov).
apply:(sincr_ofs_exten (proj1 nf) (proj1 ng)) => x ox.
set g := all_der (ord_sum2 c) b.
set s := g x y.
have os: ordinalp s by apply:(OS_all_der ha hb).
case (ord_zero_dichot oc) => cp.
by exists s => //;rewrite cp oprod0l (osum0l os).
move:(normal_ofs_compose (oprod_normal cp) (opow_normal ord_le_2omega)).
move => [sa sb]; move: (sb y ly) => /=.
set F := fun_image _ _.
have osF: (ordinal_set F).
move => t /funI_P [i iy ->]; apply:(ofs_sincr sa); ord_tac.
have ub: ordinal_ub F s.
move => t tF; move:(osF _ tF); move /funI_P: tF => [i iy ->] ot.
have liy: i <o y by ord_tac.
move:(all_der_p7 ha hb ox liy).
by rewrite (etc _ liy s os) -/g -/s; move => <-;apply: osum_Mle0.
move:(ord_ub_sup osF os ub) => pa pb; rewrite - pb in pa.
by move:(odiff_pr pa) => [ra rb]; exists (s -o c *o omega0 ^o y).
set g := all_der (ord_sum2 c) b.
set a := c *o omega0 ^o y +o x.
have yp: \0o <o y by move/limit_ordinal_P3:ly => [p2 p3].
have osa: ordinalp a by move: (OS_sum2 ov ox).
have hc: (forall i, i <o y -> all_der (ord_sum2 c) b a i = a).
move => i iy; rewrite (etc _ iy a osa).
have oi: ordinalp i by ord_tac.
have ooi := (OS_pow OS_omega oi).
have ow := OS_prod2 oc ooi.
by rewrite /a (osumA ow ov ox) - (osum_prodD ooi ooy oc) (ord_negl_p4 iy).
by move:(all_der_p8 ha hb osa yp hc) => [u ua ub]; exists u.
Qed.

Lemma all_der_ident x i (f:= fun x: Set => x)
(b:= fun x i => succ_c (card_max x i)):
ordinalp x -> ordinalp i -> all_der f b x i = x.
Proof.
set f1:= ord_sum2 \0o.
set b1 := fun x i => succ_c (card_max (omax \0o x) i).
have ha: forall x i, ordinalp x -> ordinalp i -> b1 x i = b x i.
rewrite /b /b1;move => x' i' ox oi; rewrite /omax Y_true //; ord_tac1.
move: (all_der_sum_aux OS0); rewrite -/b1 -/f1; move => [hb hc].
have sv: f1 =1o f by move => x' ox; rewrite /f1 (osum0l ox).
have sb: all_der_bound f b.
move => x' i' ox oi; rewrite - (ha _ _ ox oi).
by move: (hc _ _ ox oi) => [ua ub uc ud].
move:OS0 => oz ox oi.
rewrite - (all_der_unique hb hc sb sv ox oi) all_der_sum //.
by rewrite oprod0l (osum0l ox).
Qed.

Lemma all_der_prod c x i (f:= ord_prod2 c)
(b:= fun x i => succ_c (card_max (omax c x) i)):
\0o <o c -> ordinalp x -> ordinalp i ->
all_der f b x i = c ^o (omega0 ^o i) *o x.
Proof.
move => cp ox oi0.
have oc: ordinalp c by ord_tac.
move: (all_der_prod_aux cp); rewrite -/b; move => [ha hb].
pose p i := forall x, ordinalp x -> all_der f b x i = c ^o (omega0 ^o i) *o x.
move: x ox; rename i into i0.
apply: (least_ordinal2 (p := p)) oi0 => y oy etc.
case: (limit_ordinal_pr2 oy) => ly.
move => x ox; rewrite ly (all_der_p2 ha hb ox) opowx0 opowx1 //.
move:ly => [i oi si].
move => x ox.
have liy: i <o y by rewrite si;apply:ord_succ_lt.
have na: normal_ofs ((all_der f b)^~ i) by apply: all_der_p6.
move:(first_derivation_exten (etc _ liy) na) => eq1.
move:(all_der_p14 ha hb oi ox); rewrite - si => <- /=.
have oo1:= (OS_pow OS_omega oi).
have oo:= (opow_pos cp oo1).
rewrite (eq1 x ox) (mult_fix_enumeration oo ox) si (opow_succ OS_omega oi).
by rewrite (opow_prod oc oo1 OS_omega).
have nf:= (all_der_p6 ha hb oy).
have ooy := (OS_pow OS_omega oy).
have ov := opow_pos cp ooy.
have ng:= (oprod_normal ov).
apply:(sincr_ofs_exten (proj1 nf) (proj1 ng)) => x ox.
set g := all_der (ord_prod2 c) b.
set s := g x y.
have os: ordinalp s by apply:(OS_all_der ha hb).
case: (ord2_trichotomy oc) => c2.
by move: cp => [];rewrite c2.
by exists s => //;rewrite c2 opow1x (oprod1l os).
move: (odivision_exists1 os ov) => [q [r [oq or sv rp]]].
have op1:= (proj32_1 rp).
have op2:= (OS_prod2 op1 oq).
case: (ord_zero_dichot or) => snz.
by exists q => //; rewrite sv snz (osum0r op2).
have pc: forall i, i <o y -> c ^o (omega0 ^o i) *o r = r.
move => i iy.
have oi:= proj31_1 iy.
have ooi:= (OS_pow OS_omega oi).
have op3 := (OS_pow oc ooi).
move:(all_der_p7 ha hb ox iy).
rewrite (etc _ iy s os) -/g -/s sv (osum_prodD op2 or op3).
rewrite (oprodA op3 op1 oq) - (opow_sum oc ooi ooy) (ord_negl_p4 iy) => h.
exact: (osum2_simpl (OS_prod2 op3 or) or op2 h).
move:(normal_ofs_compose (opow_normal c2) (opow_normal ord_le_2omega)).
move => [sa sb]; move: (sb y ly) => /=.
set F := fun_image _ _.
have osF: (ordinal_set F).
move => t /funI_P [i iy ->]; apply:(ofs_sincr sa); ord_tac.
have ub: ordinal_ub F r.
move => t tF; move:(osF _ tF); move /funI_P: tF => [i iy ->] ot.
have /pc <- : i <o y by ord_tac.
apply: oprod_Mle1 => //.
move:(ord_ub_sup osF or ub) => pa pb; rewrite - pb in pa; ord_tac.
set g := all_der (ord_prod2 c) b.
set a := c ^o (omega0 ^o y) *o x.
have ovv:= (proj32_1 ov).
have yp: \0o <o y by move/limit_ordinal_P3:ly => [p2 p3].
have osa: ordinalp a by move: (OS_prod2 ovv ox).
have hc: (forall i, i <o y -> all_der (ord_prod2 c) b a i = a).
move => i iy; rewrite (etc _ iy a osa).
have oi: ordinalp i by ord_tac.
have ooi := (OS_pow OS_omega oi).
have ow := OS_pow oc ooi.
by rewrite /a (oprodA ow ovv ox) -(opow_sum oc ooi ooy) (ord_negl_p4 iy).
by move:(all_der_p8 ha hb osa yp hc) => [u ua ub]; exists u.
Qed.

Lemma all_der_prod_cor c: \2o <=o c ->
normal_ofs (fun i => c ^o (omega0 ^o i)).
Proof.
move => cp.
move: (ord2_trichotomy1 cp) => [sa sb].
have oc: ordinalp c by ord_tac.
have sc: c *o \0o = \0o by rewrite oprod0r.
have sd: c *o \1o <> \1o by rewrite (oprod1r oc).
have se: \0o <o c by ord_tac1.
have os1:= OS1.
move: (all_der_prod_aux se)=> [ha hb].
move:(all_der_p13_ter ha hb sc sd).
apply:normal_ofs_from_exten => x ox; rewrite all_der_prod // oprod1r;fprops.
Qed.

Definition Schutte_phi x y :=
all_der (ord_pow omega0) (fun x i => succ_c (card_max x i)) y x.

Lemma OS_Schutte_phi x y: ordinalp x -> ordinalp y ->
ordinalp (Schutte_phi x y).
Proof.
move: (all_der_pow_aux) => [ha hb] ox oy.
exact: (OS_all_der ha hb oy ox).
Qed.

Lemma Schutte_phi_bounded C (E :=succ_c C) x y:
infinite_c C -> inc x E -> inc y E -> inc (Schutte_phi y x) E.
Proof.
move => ic xe ye.
move: (all_der_pow_aux) => [ha hb].
move: (proj1 (CS_succ_c (proj1 ic))) => oE.
have ox: ordinalp x by ord_tac.
have oy: ordinalp y by ord_tac.
have h: card_max x y <=c C.
rewrite /card_max /omax; Ytac pa; last Ytac pb.
+ by rewrite cardinal_Bnat; apply/infinite_c_P2.
+ by move/(succ_cP (proj1 ic)): ye => [].
+ by move/(succ_cP (proj1 ic)): xe => [].
move: (omax_p2 (OS_omax ox oy)) => []; rewrite -/(card_max x y) -/C1 => sa _.
move: (proj1 (CS_succ_c (proj1 sa))) => oF.
have sc: sub (succ_c (card_max x y)) E.
move => t /(succ_cP (proj1 sa)) [sa' sb]; apply/(succ_cP (proj1 ic)).
split => //; co_tac.
by move:(all_der_p3 ha hb ox oy) => /sc.
Qed.

Lemma Schutte_phi_countable x y:
countable_ordinal x -> countable_ordinal y ->
countable_ordinal (Schutte_phi x y).
Proof.
move => /aleph_oneP xa /aleph_oneP ya; apply/aleph_oneP.
by apply:Schutte_phi_bounded => //; apply: omega_infinitec.
Qed.

Lemma Schutte_phi_p0 x: ordinalp x -> Schutte_phi \0o x = omega0 ^o x.
Proof.
move: (all_der_pow_aux) => [ha hb].
move => ox; exact: (all_der_p2 ha hb ox).
Qed.

Lemma Schutte_phi_p1 x: ordinalp x -> normal_ofs (Schutte_phi x).
Proof.
move: (all_der_pow_aux) => [ha hb].
move => ox; exact: (all_der_p6 ha hb ox).
Qed.

Lemma Schutte_phi_p2 x: ordinalp x ->
first_derivation (Schutte_phi x) =1o (Schutte_phi (succ_o x)).
Proof.
move: (all_der_pow_aux) => [ha hb].
move => ox; exact: (all_der_p14 ha hb ox).
Qed.

Lemma Schutte_phi_p3 x i j: ordinalp x -> i <o j ->
Schutte_phi i (Schutte_phi j x) = Schutte_phi j x.
Proof.
move: (all_der_pow_aux) => [ha hb] ox ij.
exact: (all_der_p7 ha hb ox ij).
Qed.

Lemma Schutte_phi_p4 y j: ordinalp y -> \0o <o j ->
(forall i, i <o j -> Schutte_phi i y = y) ->
(exists2 x, ordinalp x & y = Schutte_phi j x).
Proof.
move: (all_der_pow_aux) => [ha hb] oy jp h.
exact:(all_der_p8 ha hb oy jp h).
Qed.

Lemma Schutte_phi_p5 : normal_ofs (Schutte_phi ^~ \0o).
Proof.
move: (all_der_pow_aux) => [ha hb].
have hc: omega0 ^o \0o <> \0o by apply: omega_pow_nz; fprops.
exact:(all_der_p13 ha hb hc).
Qed.

Lemma Schutte_phi_p6 x y i j:
ordinalp x -> ordinalp y -> ordinalp i -> ordinalp j ->
(Schutte_phi i x = Schutte_phi j y <->
[/\ i <o j -> x = Schutte_phi j y,
i = j -> x = y &
j <o i -> y = Schutte_phi i x]).
Proof.
move: (all_der_pow_aux) => [ha hb] ox oy oi oj.
exact: (all_der_p9 ha hb ox oy oi oj ).
Qed.

Lemma Schutte_phi_p7 x y i j:
ordinalp x -> ordinalp y -> ordinalp i -> ordinalp j ->
(Schutte_phi i x <o Schutte_phi j y <->
[/\ i <o j -> x <o Schutte_phi j y,
i = j -> x <o y &
j <o i -> Schutte_phi i x <o y]).
Proof.
move: (all_der_pow_aux) => [ha hb] ox oy oi oj.
exact: (all_der_p10 ha hb ox oy oi oj ).
Qed.

Lemma Schutte_phi_p8 x y i j:
ordinalp x -> ordinalp y -> ordinalp i -> ordinalp j ->
(Schutte_phi i x <=o Schutte_phi j y <->
[/\ i <o j -> x <=o Schutte_phi j y,
i = j -> x <=o y &
j <o i -> Schutte_phi i x <=o y]).
Proof.
move: (all_der_pow_aux) => [ha hb] ox oy oi oj.
exact: (all_der_p10' ha hb ox oy oi oj ).
Qed.

Definition Schutte_Cr a b := exists2 x, ordinalp x & b = Schutte_phi a x.

Lemma Schutte_Cr_p1 a (p:= Schutte_Cr a): ordinalp a ->
(iclosed_collection p /\ non_coll p).
Proof.
move => oa; move: (Schutte_phi_p1 oa) => sa.
by apply: iclosed_normal_ofs.
Qed.

Lemma Schutte_Cr_p2 a (p:= Schutte_Cr a): ordinalp a ->
ordinalsf p =1o Schutte_phi a.
Proof.
move => oa.
move: (Schutte_Cr_p1 oa)=> [sa sb].
move: (ordinals_col_p2 sa sb); rewrite -/p => sc.
move: (Schutte_phi_p1 oa) => sd.
move: (ordinals_col_p1 (proj1 sa) sb) => [ha hb _ _ _].
apply: (sincr_ofs_exten (proj1 sc) (proj1 sd)) => x ox.
exact (ha _ ox).
by apply: hb; rewrite /p /Schutte_Cr; exists x.
Qed.

Lemma Schutte_Cr_p3 b: ordinalp b ->
(Schutte_Cr \0o b <-> ord_indecomposable b).
Proof.
move => ob; split.
by move => [x ox ->]; rewrite (Schutte_phi_p0 ox); apply:indecomp_prop4.
move /indecomp_prop3 => [y oy ->]; rewrite - (Schutte_phi_p0 oy).
by exists y.
Qed.

Lemma Schutte_Cr_p4 a b: \0o <o a -> ordinalp b ->
(Schutte_Cr a b <-> (forall c, c <o a -> Schutte_phi c b = b)).
Proof.
move => ap ob; split.
by move => [x ox ->] c ca; apply: Schutte_phi_p3.
by move /(Schutte_phi_p4 ob ap).
Qed.

Lemma Schutte_Cr_p5 a b: limit_ordinal a -> ordinalp b ->
(Schutte_Cr a b <-> (forall c, c <o a -> Schutte_Cr c b)).
Proof.
move => ap ob; split.
move => [x ox ->] c ca; exists (Schutte_phi a x).
apply: OS_Schutte_phi => //; ord_tac.
by symmetry; apply: Schutte_phi_p3.
move /limit_ordinal_P3: ap => [sa sb sc].
apply:Schutte_phi_p4 => //.
move => i ia; move:(sc _ (sb _ ia)) => [x ox xv].
move:(Schutte_phi_p3 ox (ord_succ_lt (proj31_1 ia))).
by rewrite - xv.
Qed.

Lemma Schutte_Cr_p6 a b: ordinalp a -> ordinalp b ->
(Schutte_Cr (succ_o a) b <-> Schutte_phi a b = b).
Proof.
move => oa ob.
have osa := OS_succ oa.
have sa: \0o <o succ_o a by apply: ord_ne0_pos => //;apply: succo_nz.
have asa:= (ord_succ_lt oa).
split; first by move/(Schutte_Cr_p4 sa ob) => h; exact: (h a asa).
move => aux.
apply/(Schutte_Cr_p4 sa ob) => c /ord_lt_succP ca.
case: (equal_or_not c a) => eca; first by rewrite eca.
by rewrite - aux; apply: Schutte_phi_p3.
Qed.

Lemma Schutte_Cr_p7 a a' b: a <=o a' -> ordinalp b ->
Schutte_Cr a' b -> Schutte_Cr a b.
Proof.
move => aa ob pa.
case: (equal_or_not a a') => h; first by rewrite h.
move: pa => [x ox ->]; exists ( Schutte_phi a' x) => //.
by apply: OS_Schutte_phi => //; ord_tac.
by symmetry; apply:Schutte_phi_p3.
Qed.

Lemma Schutte_Cr_p8 a b: ordinalp a -> ordinalp b ->
Schutte_Cr a b -> ord_indecomposable b.
Proof.
move => oa ob h.
have ap: \0o <=o a by ord_tac1.
by move: (Schutte_Cr_p7 ap ob h); move /(Schutte_Cr_p3 ob).
Qed.

Lemma Schutte_Cr_p8' a b: ordinalp a -> ordinalp b ->
ord_indecomposable (Schutte_phi a b).
Proof.
by move => oa ob; apply (Schutte_Cr_p8 oa (OS_Schutte_phi oa ob)); exists b.
Qed.

Lemma Schutte_phi_p9 x: ordinalp x -> x <=o Schutte_phi x \0o.
Proof.
move => ox; move: (Schutte_phi_p5) => h; exact:(osi_gex (proj1 h) ox).
Qed.

Lemma Schutte_Cr_p9 x y: ordinalp x -> ordinalp y -> Schutte_Cr x y ->
x <=o y.
Proof.
move => ox oy [z oz ->].
move: (Schutte_phi_p9 ox) => h.
case (ord_zero_dichot oz) => eq; first by rewrite eq.
move: (proj1 (Schutte_phi_p1 ox) _ _ eq) => [le _]; ord_tac.
Qed.

Lemma Schutte_phi_p10a a b a' b' x:
ordinalp a -> b <o x -> x = Schutte_phi a b ->
ordinalp a' -> b' <o x -> x = Schutte_phi a' b' ->
(a = a' /\ b = b').
Proof.
move => oa p2 p3 oa' q2 q3.
rewrite p3 in q3.
move/ (Schutte_phi_p6 (proj31_1 p2) (proj31_1 q2) oa oa'): (q3).
move => [sa sb sc].
case: (ord_le_to_ell oa oa') => h; first by split => //; apply: sb.
by move: (sa h) p2; rewrite - q3 - p3 => ->; move => [].
by move: (sc h) q2; rewrite - p3 => ->; move => [].
Qed.

Lemma Schutte_phi_p10b x: ord_indecomposable x ->
(exists a b, [/\ a <=o x, b <o x & x = Schutte_phi a b]).
Proof.
move => ix; move: (ix) => [xp _].
have ox: ordinalp x by ord_tac.
move: (proj1 (Schutte_phi_p1 ox) _ _ xp) => sa.
move: (ord_le_ltT (Schutte_phi_p9 ox) sa) => sb.
pose p a:= Schutte_phi a x = x.
have npa: not (p x) by move => h; move: sb => []; rewrite h.
move: (least_ordinal3 ox npa (p := p)).
set a := least_ordinal _ x; move => [oa nn etc].
case: (ord_le_to_el oa ox); [move => ax | by move => /etc px].
have [b ob xv]: exists2 b, ordinalp b & x = Schutte_phi a b.
case: (ord_zero_dichot oa) => az.
by rewrite az;move/(Schutte_Cr_p3 ox): ix.
apply:(Schutte_phi_p4 ox az etc).
have ica := (proj1 (Schutte_phi_p1 oa)).
have xaxx := (osi_gex ica ox).
have h: x <o Schutte_phi a x by split => // eq; case nn.
exists a,b ; split => //.
case: (ord_le_to_ell ox ob).
+ by move => eq; move: (proj2 h); rewrite {2} eq.
+ move => xb; move: (proj1(ica _ _ xb)); rewrite - xv.
move=> lt2; ord_tac.
+ done.
Qed.

Definition strong_critical x := Schutte_Cr x x.

Lemma strong_criticalP x: ordinalp x ->
(strong_critical x <-> Schutte_phi x \0o = x).
Proof.
move => ox;split; last by move => h; exists \0o; fprops.
move => [y oy yb]; move: (Schutte_phi_p9 ox); rewrite {1} yb => h.
case: (ord_zero_dichot oy); first by move => <-.
move/ (proj1 (Schutte_phi_p1 ox)) => h'; ord_tac.
Qed.

Lemma strong_critical_closed_noncol
(p := fun z => ordinalp z /\ strong_critical z):
(iclosed_collection p /\ non_coll p).
Proof.
move: Schutte_phi_p5;set f := (Schutte_phi^~ \0o) => nf.
move: (iclosed_fixpoints nf) => [[pa pb] pc].
have aux: forall z, p z <-> (ordinalp z /\ f z = z).
move => z; split.
by move => [oz] /( strong_criticalP oz) => h.
by move => [oz] /( strong_criticalP oz) => h.
split => //; first split.
+ by move => x [].
+ by move => g pF nef; apply /aux; apply: pb => // x/pF => w; apply/aux.
+ by move => [E ev]; case:pc; exists E => x; split; [move/ev/aux| move/aux/ev].
Qed.

Definition Gamma_0 := the_least_fixedpoint_ge (Schutte_phi ^~ \0o) \0o.

Lemma Gamma0_p :
Schutte_phi Gamma_0 \0o = Gamma_0 /\
forall x, ordinalp x -> Schutte_phi x \0o = x -> Gamma_0 <=o x.
Proof.
move: (normal_ofs_fix Schutte_phi_p5 OS0); rewrite -/Gamma_0.
move => [sa sb sc]; split => // x ox; apply: sc; ord_tac1.
Qed.

Lemma countable_Gamma_0: countable_ordinal Gamma_0.
Proof.
move: omega_infinitec => sa.
move: Schutte_phi_p5 => sb.
move: (succ_c_zero sa) => sc.
have sd: (forall x, inc x aleph_one -> inc ((Schutte_phi^~ \0o) x) aleph_one).
by move => x xa; apply:Schutte_phi_bounded.
by move: (next_fix_point_small sa sb sd sc) => /aleph_oneP.
Qed.

Lemma Gamma0_s x y: x <o Gamma_0 -> y <o Gamma_0 -> Schutte_phi x y <o Gamma_0.
Proof.
move => sa sb.
move: Gamma0_p => [sc sd].
move: (proj31_1 sa) => ox.
move: (proj31_1 sb) => oy.
move: (proj32_1 sb) => og.
rewrite - sc.
apply/(Schutte_phi_p7 oy OS0 ox og); split.
+ by rewrite sc.
+ by move: (proj2 sa).
+ by move => [h]; ord_tac.
Qed.

Lemma Gamma0_limit: limit_ordinal Gamma_0.
Proof.
move: (proj1 Gamma0_p) => h.
have og:= (proj1 (countable_Gamma_0)).
have lo:=omega_limit.
case:(indecomp_limit (Schutte_Cr_p8' og OS0)); rewrite h// => h2.
move: h; rewrite h2 => h3.
move: (Schutte_phi_p3 OS0 (ord_lt_01)).
rewrite h3 (Schutte_phi_p0 OS1) opowx1; [ by move => <- | fprops].
Qed.

Lemma Gamma0_epsilon: omega0 ^o Gamma_0 = Gamma_0.
Proof.
move: Gamma0_p => [g1 g2].
move: (limit_positive (Gamma0_limit)) => sa.
move: (Schutte_phi_p3 OS0 sa); rewrite g1 (Schutte_phi_p0) //; ord_tac.
Qed.

Definition Schutte_zeta :=
induction_term (fun (n:Set) v => Schutte_phi v \0o) \1o.

Lemma Schutte_zeta_0: Schutte_zeta \0c = \1o.
Proof. exact: induction_term0. Qed.

Lemma Schutte_zeta_1: Schutte_zeta \0c = Schutte_phi \0o \0o.
Proof. by rewrite Schutte_zeta_0 (Schutte_phi_p0 OS0) opowx0. Qed.

Lemma Schutte_zeta_2 n: inc n Bnat ->
Schutte_zeta (succ n) = Schutte_phi (Schutte_zeta n) \0o.
Proof.
apply: (induction_terms (fun (n:Set) v => Schutte_phi v \0o) \1o).
Qed.

Lemma OS_Schutte_zeta n: inc n Bnat -> ordinalp (Schutte_zeta n).
Proof.
move:n;apply: cardinal_c_induction.
rewrite Schutte_zeta_0; fprops.
move => n nb Hrec; rewrite (Schutte_zeta_2 nb); apply:OS_Schutte_phi; fprops.
Qed.

Lemma Schutte_zeta_3 n: inc n Bnat -> Schutte_zeta n <o Gamma_0.
Proof.
move: n; apply:cardinal_c_induction.
move: Gamma0_limit (ord_lt_1omega) => /omega_limit2 ha hb.
rewrite Schutte_zeta_0; ord_tac.
move => n nb Hrec; rewrite (Schutte_zeta_2 nb).
by rewrite -(proj1 (Gamma0_p)); move: (proj1 (Schutte_phi_p5) _ _ Hrec).
Qed.

Lemma Schutte_zeta_4 k: inc k Bnat ->
Schutte_zeta k <o Schutte_zeta (succ k).
Proof.
move => kb; rewrite (Schutte_zeta_2 kb); move:(OS_Schutte_zeta kb) => ox.
split; first exact:(Schutte_phi_p9 ox).
move => eq.
move: (proj2 (Gamma0_p) _ ox (sym_eq eq)) (Schutte_zeta_3 kb) => ha hb; ord_tac.
Qed.

Lemma Schutte_zeta_5 n m: inc n Bnat -> inc m Bnat -> n <c m ->
Schutte_zeta n <o Schutte_zeta m.
Proof.
move => nB mB nm.
have pa: forall k, inc k Bnat -> k <> \0c ->
Schutte_zeta n <o Schutte_zeta (n +c k).
apply: cardinal_c_induction => //.
move => k kb Hrec _; rewrite (csum_via_succ _ kb).
have hh: Schutte_zeta (n +c k) <o Schutte_zeta (succ (n +c k)).
apply:Schutte_zeta_4; fprops.
case (equal_or_not k \0c) => kz.
move: hh; rewrite {1} kz csum0r //; fprops.
move: (proj1 (Hrec kz)) => ha; ord_tac.
move: (cdiff_pr (proj1 nm)) => <-.
apply: pa; [fprops | exact: (cdiff_nz nm) ].
Qed.

Lemma Schutte_zeta_6 x: ordinalp x ->
(forall n, inc n Bnat -> Schutte_zeta n <=o x) -> Gamma_0 <=o x.
Proof.
move => ox pa.
move: (induction_defined_pr (Schutte_phi^~ \0o) \0o).
rewrite /Gamma_0 /the_least_fixedpoint_ge.
set f := induction_defined _ _.
move => [sf sjf f0 fsn].
have f1: Vf f (succ \0c) = Schutte_zeta \0o.
by rewrite (fsn _ BS0) f0 - Schutte_zeta_1.
have pb: forall n, inc n Bnat -> (Vf f (succ n)) = Schutte_zeta n.
apply: cardinal_c_induction => // n nB hr.
by rewrite (fsn _ (BS_succ nB)) hr (Schutte_zeta_2 nB).
have aux: forall t, inc t (target f) -> t = \0o \/
(exists2 n, inc n Bnat & t = Schutte_zeta n).
move => i /(proj2 sjf) [n]; rewrite sf => nb <-.
case (equal_or_not n \0o) => nz; [by rewrite nz f0; left | right].
move: (cpred_pr nb nz) => [qa qb]; ex_tac.
by rewrite {1} qb pb.
apply:ord_ub_sup => //.
move => i /aux; case; first by move => ->; fprops.
by move => [n /OS_Schutte_zeta h ->].
by move => i /aux; case; [ move => ->;ord_tac1 | move => [n nb ->]; apply:pa].
Qed.

Lemma Schutte_14_16' x: x <o Gamma_0 ->
exists2 n, inc n Bnat & x <o Schutte_zeta n.
Proof.
move: (proj31_1 h) => ox.
have: (forall n, inc n Bnat -> Schutte_zeta n <=o x).
move => n nb; ex_middle b; case bad; exists n => //.
case: (ord_le_to_el (OS_Schutte_zeta nb) ox) => //.
move/(Schutte_zeta_6 ox) => ha; ord_tac.
Qed.

Lemma Schutte_14_16 x: x <o Gamma_0 ->
exists2 n, inc n Bnat & x <o Schutte_zeta n.
Proof.
move => h.
pose p x :=x <o Gamma_0 -> exists2 n, inc n Bnat & x <o Schutte_zeta n.
apply:(least_ordinal2 (p := p)) (proj31_1 h) h => y oy Hr yg.
case (ord_zero_dichot oy).
move => ->; exists \0o; fprops; rewrite Schutte_zeta_0; apply:ord_lt_01.
move=> yp.
move: (omega_log_p1 yp) => [z [oz pa pb]].
move: (Schutte_phi_p10b (indecomp_prop4 oz)) => [a [b [az bz etc]]].
move: (proj2 Gamma0_p) => gp.
move: (proj31_1 bz) (proj31 az) => ob oa.
move: (ord_le_ltT (ord_leT az pa) yg) => ag0.
move: (ord_le_ltT (ord_leT (proj1 bz) pa) yg) => bg0.
have az': a <o omega0 ^o z.
split => //; rewrite etc => e1.
case (ord_zero_dichot ob) => bez.
have eq2: Schutte_phi a \0o = a by rewrite - bez.
move: (gp _ oa eq2) => ga ; ord_tac.
move: (proj1 (Schutte_phi_p1 oa) _ _ bez); rewrite - e1.
move: (osi_gex (proj1(Schutte_phi_p5)) oa) => ga gb; ord_tac.
move: (ord_lt_leT bz pa) => lby.
move: (ord_lt_leT az' pa) => lay.
move: (Hr _ lby bg0) (Hr _ lay ag0)=> [n nB nb] [m mB ma].
set nm:= Yo (n <=c m) m n.
have nmB: inc nm Bnat by rewrite /nm;Ytac w.
have laS: a <o Schutte_zeta nm.
rewrite /nm; Ytac w => //.
case: (card_le_to_el (CS_Bnat nB) (CS_Bnat mB)) => // lmn.
move: (Schutte_zeta_5 mB nB lmn) => h1; ord_tac.
have lbS: b <o Schutte_zeta nm.
rewrite /nm; Ytac w => //; case (equal_or_not n m) => ee; try ue.
move: (Schutte_zeta_5 nB mB (conj w ee)) => h1; ord_tac.
have lt1: omega0 ^o z <o Schutte_zeta (succ nm).
rewrite etc (Schutte_zeta_2 nmB).
apply/(Schutte_phi_p7 ob OS0 oa (proj32_1 laS)); split.
+ move: (Schutte_zeta_4 nmB); rewrite (Schutte_zeta_2 nmB) => h1 _; ord_tac.
+ by move => e1; move: (proj2 laS); rewrite - e1.
+ by move => [e1 _]; ord_tac.
exists (succ nm); first by fprops.
have [u ou uv]: exists2 u, ordinalp u & Schutte_zeta (succ nm) = omega0 ^o u.
move: (proj32_1 laS) OS0 => o1 o2.
by apply: indecomp_prop3;rewrite (Schutte_zeta_2 nmB); apply:Schutte_Cr_p8'.
move: lt1; rewrite uv.
case: (ord_le_to_el ou oz); first by move/opow_Momega_le => ha hb; ord_tac.
move/(ord_succ_ltP) => /opow_Momega_le pc _; ord_tac.
Qed.

Definition maximal_critical a x :=
Schutte_Cr a x /\ forall a', a <o a' -> ~ Schutte_Cr a' x.

Lemma maximal_criticalP a x: ordinalp a -> ordinalp x ->
(maximal_critical a x <-> exists2 b, b<o x & x = Schutte_phi a b).
Proof.
move => oa ox; split.
move=> [[c oc cv] pb]; exists c => //.
have ica:= (proj1 (Schutte_phi_p1 oa)).
move:(osi_gex ica oc); rewrite - cv => cx; split => // ecx.
rewrite ecx in cv.
by case:(pb _ (ord_succ_lt oa)); apply/(Schutte_Cr_p6 oa ox).
move => [b bx bv]; split; first by exists b => //; ord_tac.
move => c ac [d od dv].
rewrite dv in bv.
move/(Schutte_phi_p6 od (proj31_1 bx) (proj32_1 ac) oa): bv.
by move => [_ _ h]; move: (h ac) (proj2 bx); rewrite - dv.
Qed.

Lemma maximal_critical_p1 x: ord_indecomposable x ->
exists2 a, ordinalp a & maximal_critical a x.
Proof.
move => ix; move: (Schutte_phi_p10b ix) => [a [b [pa pb pc]]].
have oa: ordinalp a by ord_tac.
by exists a => //; apply/(maximal_criticalP oa (proj32 pa)); exists b.
Qed.

Definition Schutte_psi_aux a b :=
exists n c, [/\ n <o omega0, ordinalp c, b = c +o n & Schutte_phi a c = c].
Definition Schutte_psi a b :=
Schutte_phi a (Yo (Schutte_psi_aux a b) (succ_o b) b).

Lemma OS_Schutte_psi a b: ordinalp a -> ordinalp b ->
ordinalp (Schutte_psi a b).
Proof.
move => oa ob; apply: (OS_Schutte_phi oa); Ytac h;fprops.
Qed.

Lemma Schutte_psi_p0 a: ordinalp a ->
Schutte_psi a \0o = Schutte_phi a \0o.
Proof.
move => oa; rewrite /Schutte_psi; Ytac h => //.
move: h => [n [c [on oc eq1]]].
move: (osum2_zero oc (proj31_1 on) (sym_eq eq1)) => [-> _] eq2.
by move:(proj2(proj1 (Schutte_Cr_p8' oa OS0))); rewrite eq2.
Qed.

Lemma Gamma0_s_psi a b: a <o Gamma_0 -> b <o Gamma_0 ->
Schutte_psi a b <o Gamma_0.
Proof.
move => pa pb; rewrite /Schutte_psi; Ytac h; apply:Gamma0_s => //.
by move /limit_ordinal_P3: Gamma0_limit => [_ ]; apply.
Qed.

Lemma Schutte_psi_p1 a b b':
ordinalp a -> ordinalp b -> ordinalp b' ->
(Schutte_psi a b = Schutte_phi a b') -> b' <o Schutte_phi a b'.
Proof.
move => oa ob ob'; rewrite /Schutte_psi => sa.
have ica:= (proj1 (Schutte_phi_p1 oa)).
have pa:= (osi_gex ica ob).
have: (Yo (Schutte_psi_aux a b) (succ_o b) b) = b'.
have oy: ordinalp (Yo (Schutte_psi_aux a b) (succ_o b) b) by Ytac h; fprops.
by move/(Schutte_phi_p6 oy ob' oa oa): sa => [_ h _]; apply:h.
Ytac h0 => eq2.
move:(ord_le_ltT pa (ica _ _ (ord_succ_lt ob)));rewrite -{1} eq2 {1} eq2.
case:(indecomp_limit (Schutte_Cr_p8' oa ob')).
move => -> /ord_lt1 bz.
move: h0 => [n [c [qa qb qc]]].
have cnz: c +o n = \0o by rewrite - bz.
move: (osum2_zero qb (proj31_1 qa) cnz) => [-> _] e2.
by move: (Schutte_Cr_p8' oa OS0) => [] []; rewrite e2.
move => /limit_ordinal_P3 [_]; apply.
rewrite - eq2;split => // eq1; case h0; exists \0o, b; rewrite (osum0r ob).
split => //; exact:ord_lt_0omega.
Qed.

Lemma Schutte_psi_p1' a b (b' := (Yo (Schutte_psi_aux a b) (succ_o b) b)):
ordinalp a -> ordinalp b -> b' <o Schutte_phi a b'.
Proof.
move => oa ob.
have ob':ordinalp b' by rewrite /b'; Ytac h; fprops.
by apply: (Schutte_psi_p1 oa ob ob').
Qed.

Lemma Schutte_psi_p2 a b: ordinalp a -> ordinalp b ->
b <o Schutte_psi a b.
Proof.
move => oa ob.
move: (Schutte_psi_p1' oa ob).
rewrite /Schutte_psi; set c := Yo _ _ _ => e1.
suff : b <=o c by move => bc; ord_tac.
rewrite /c; Ytac h; [ apply: (proj1(ord_succ_lt ob)) | ord_tac].
Qed.

Lemma Schutte_psi_p3 a b b':
ordinalp a -> b <o b' -> (Schutte_psi a b <o Schutte_psi a b').
Proof.
move => oa bb'; rewrite /Schutte_psi.
have sbb: succ_o b <o succ_o b' by move/ord_lt_succ_succP: bb'.
apply: (proj1 (Schutte_phi_p1 oa)).
Ytac pa; Ytac pb => //.
split; first by move/ord_succ_ltP: bb'.
move => h; move: pa => [n [c [qa qb qc qd]]]; case: pb.
exists (succ_o n), c; split => //.
by move: omega_limit => /limit_ordinal_P3 [_]; apply.
rewrite -h qc osum2_succ=> //; ord_tac.
move:(proj1 (ord_succ_lt (proj32_1 bb'))) => h; ord_tac.
Qed.

Lemma Schutte_psi_p4 a a' b b':
ordinalp a -> ordinalp a' -> ordinalp b -> ordinalp b' ->
(Schutte_psi a b = Schutte_psi a' b') ->
(a = a' /\ b = b').
Proof.
move=> oa oa' ob ob' eq.
move: (Schutte_psi_p1' oa ob); set c := Yo _ _ _.
move: (Schutte_psi_p1' oa' ob'); set c' := Yo _ _ _.
move => sa sb.
move /(Schutte_phi_p6 (proj31_1 sb) (proj31_1 sa) oa oa') : (eq).
move => [qa qb qc].
have eq0:Schutte_phi a c = Schutte_phi a' c' by [].
case: (ord_le_to_ell oa oa') => h.
+ case: (ord_le_to_ell ob ob') => h'; first by split.
by move:( Schutte_psi_p3 oa h') => []; rewrite eq h.
by move:( Schutte_psi_p3 oa h') => []; rewrite eq h.
+ by move: (qa h); move: sb => []; rewrite - eq0.
+ by move: (qc h); move: sa => []; rewrite eq0.
Qed.

Lemma Schutte_psi_p5 a b: ordinalp a -> ordinalp b ->
(a <o Schutte_psi a b <-> ~ (strong_critical (Schutte_psi a b))).
Proof.
move => oa ob; set c :=Schutte_psi a b.
have oc: ordinalp c by apply: OS_Schutte_psi.
case (equal_or_not (Schutte_phi c \0o) c) => eq1.
split; last by move => h; move/(strong_criticalP oc): eq1.
move:(Schutte_psi_p0 oc); rewrite eq1; move/(Schutte_psi_p4 oc oa OS0 ob).
by move => [-> _] [_].
split; first by move => _ h; move/(strong_criticalP oc): eq1.
move => _.
have: c <o Schutte_phi c \0o.
split; [ exact:(osi_gex (proj1 (Schutte_phi_p5)) oc) | by apply:nesym].
rewrite{1}/c /Schutte_psi. set d := Yo _ _ _.
have od: ordinalp d.
rewrite /d; Ytac h; fprops.
move/(Schutte_phi_p7 od OS0 oa oc) => [qa qb qc].
case (ord_le_to_ell oa oc) => // h.
by move: (qb h) => /ord_lt0.
by move: (qc h) => /ord_lt0.
Qed.

Lemma Schutte_psi_p6 a b: a <o Gamma_0 -> b <o Gamma_0 ->
a <o Schutte_psi a b.
Proof.
move => pa pb.
have oa: ordinalp a by ord_tac.
have ob: ordinalp b by ord_tac.
have oc:= (OS_Schutte_psi oa ob).
move: (Gamma0_s_psi pa pb) => h.
apply/(Schutte_psi_p5 oa ob) => /(strong_criticalP oc) h1.
move: (proj2 Gamma0_p _ oc h1) => h2; ord_tac.
Qed.

Lemma Schutte_psi_p7 x: ord_indecomposable x ->
(exists a b, [/\ a <=o x, b <o x & x = Schutte_psi a b]).
Proof.
move => oix.
move:(Schutte_phi_p10b oix) => [a [b [pa pb pc]]].
move: (pb) => [[ob ox _] _].
case: (p_or_not_p (Schutte_psi_aux a b)); last first.
by move => h; exists a,b ; split => //; rewrite /Schutte_psi; Ytac0.
move => [n [c [oi oc pd pe]]].
have on: ordinalp n by ord_tac.
case: (limit_ordinal_pr2 on) => nz.
+ have bc: b = c by move: pd; rewrite nz (osum0r oc).
move: pe (proj2 pb); rewrite - bc - pc => -> //.
+ move: (predo_K on nz); set m := \opred n => sm.
have om: ordinalp m by apply:OS_sup => t tn; ord_tac.
have ocm:= OS_sum2 oc om.
have le1: c +o m <o x.
have: c +o m <=o c +o n.
apply:osum_Meqle => //; rewrite - sm; exact: (proj1 (ord_succ_lt om)).
rewrite - pd => sa; ord_tac.
have spa: (Schutte_psi_aux a (c +o m)).
exists m, c; split => //; move: (ord_succ_lt om); rewrite sm =>h; ord_tac.
exists a, (c +o m); split => //;rewrite /Schutte_psi; Ytac0.
by rewrite osum2_succ // sm - pd.
move:(omega_limit2 nz) => h; ord_tac.
Qed.

Lemma Schutte_psi_p2' a b: ordinalp a -> ordinalp b ->
a <=o Schutte_psi a b.
Proof.
move => oa ob.
have: ord_indecomposable (Schutte_psi a b).
rewrite /Schutte_psi; Ytac h; apply:Schutte_Cr_p8'; fprops.
move/ (Schutte_psi_p7) => [a' [b' [p1 p2 p3]]].
move: (Schutte_psi_p4 oa (proj31 p1) ob (proj31_1 p2) p3).
by move => [e1 e2]; rewrite {1} e1.
Qed.

Definition inv_psi_omega x:=
select (fun z => Schutte_psi (P z) (Q z) = (omega0 ^o x))
(coarse (succ_o (omega0 ^o x))).

Lemma inv_psi_omega_p x (z:=omega0 ^o x) (y:= inv_psi_omega x) :
ordinalp x ->
[/\ pairp y, (P y) <=o z, (Q y) <o z & Schutte_psi (P y) (Q y) = z].
Proof.
move => ox.
pose p z:= (Schutte_psi (P z) (Q z) = (omega0 ^o x)).
set E := (coarse (succ_o (omega0 ^o x))).
have oo: ordinalp (omega0 ^o x) by fprops.
move: (OS_succ oo) => osx.
have pb:singl_val2 (inc^~ E) p.
move => y1 y2 /setX_P [ra rb rc] e1 /setX_P [ra' rb' rc'].
rewrite /p - e1 => e2.
have o1: ordinalp (P y1) by ord_tac.
have o2: ordinalp (P y2) by ord_tac.
have o3: ordinalp (Q y1) by ord_tac.
have o4: ordinalp (Q y2) by ord_tac.
move:(Schutte_psi_p4 o2 o1 o4 o3 e2) => [rd re].
by apply: pair_exten.
move: (Schutte_psi_p7 (indecomp_prop4 ox)) => [a [b [p1 p2 p3]]].
have p4: (inc (J a b) E).
move:(p2) =>[p2' _]; apply/setX_P; aw; split; fprops; by apply/ord_leP.
have p5: p (J a b) by rewrite /p; aw.
move: (select_uniq pb p4 p5); rewrite /y /inv_psi_omega. move => <-; aw.
split;fprops.
Qed.

Lemma Schutte_psi_p8 a b:
ordinalp a -> ordinalp b -> (maximal_critical a (Schutte_psi a b)).
Proof.
move => oa ob.
have[c oc h]: exists2 c, ordinalp c & Schutte_psi a b = Schutte_phi a c.
by rewrite /Schutte_psi; Ytac h; [ exists (succ_o b); fprops | exists b].
apply/ (maximal_criticalP oa (OS_Schutte_psi oa ob)); exists c => //.
rewrite h;exact: (Schutte_psi_p1 oa ob oc h).
Qed.

Definition olog x := select (fun z => omega0 ^o z = x) (succ_o x).

Lemma ologp x: ordinalp x -> olog (omega0 ^o x) = x.
Proof.
move => ox.
pose p z:= (omega0 ^o z = omega0 ^o x).
set E := (succ_o (omega0 ^o x)).
have oo: ordinalp (omega0 ^o x) by fprops.
have pb:singl_val2 (inc^~ E) p.
move => /= y1 y2 y1e e1 y2e.
rewrite /p - e1 => e2.
move/(ord_leP oo): y1e => [o1 _ _].
move/(ord_leP oo): y2e => [o2 _ _].
by move:(opow_regular ord_le_2omega o2 o1 e2).
have p4: (inc x E) by apply/(ord_leP oo); apply:(opow_Mspec ord_le_2omega ox).
have p5: p x by [].
by move: (select_uniq pb p4 p5).
Qed.

Lemma ologp_psi a b: ordinalp a -> ordinalp b ->
(ordinalp (olog (Schutte_psi a b)) /\
omega0 ^o olog (Schutte_psi a b) = (Schutte_psi a b)).
Proof.
move => oa ob.
have: ord_indecomposable (Schutte_psi a b).
rewrite /Schutte_psi; Ytac h; apply:Schutte_Cr_p8'; fprops.
by move/indecomp_prop3 => [y oy ->]; rewrite(ologp oy).
Qed.

Lemma Schutte_psi_p9 a b: ordinalp a -> ordinalp b ->
(maximal_critical a b <-> (exists2 c, ordinalp c & b = Schutte_psi a c)).
Proof.
move => oa ob; split; last by move => [c oc ->]; apply:Schutte_psi_p8.
move => /(maximal_criticalP oa ob) [c ca eq].
have oc: ordinalp c by ord_tac.
case: (p_or_not_p (Schutte_psi_aux a c)); last first.
by move => h; exists c => //; rewrite /Schutte_psi; Ytac0.
move => [n [d [oi od pd pe]]].
have on: ordinalp n by ord_tac.
case: (limit_ordinal_pr2 on) => nz.
+ have bc: c = d by move: pd; rewrite nz (osum0r od).
by move: pe (nesym (proj2 ca)); rewrite - bc - eq.
+ move: (predo_K on nz); set m := \opred n => sm.
have om: ordinalp m by apply:OS_sup => t tn; ord_tac.
have ocm:= OS_sum2 od om.
have spa: (Schutte_psi_aux a (d +o m)).
exists m, d; split => //; move: (ord_succ_lt om); rewrite sm =>h; ord_tac.
exists (d +o m) => //;rewrite /Schutte_psi; Ytac0.
by rewrite osum2_succ // sm - pd.
move:(omega_limit2 nz) => h; ord_tac.
Qed.

Lemma Schutte_psi_p10 a: ordinalp a -> ~(normal_ofs (Schutte_psi a)).
Proof.
move => oa [pa pb].
set x := Schutte_phi (succ_o a) \0o.
case:(indecomp_limit (Schutte_Cr_p8' (OS_succ oa) OS0)).
move: (ord_succ_lt oa)=> lt1 e1.
move: (Schutte_phi_p3 OS0 lt1); rewrite e1 => e2.
have ica:= (proj1 (Schutte_phi_p1 oa)).
move: (ica _ _ ord_lt_01); rewrite e2;move/ord_lt1 => e3.
by move:(Schutte_Cr_p8' oa OS0) => [][]; rewrite e3.
rewrite -/x => limx; move: (proj31 limx ) => ox.
move:(Schutte_phi_p1 oa)=> [pa' pb'].
have pc: forall t, t<o x -> Schutte_phi a t <> t.
move => t tx eq.
have ot: ordinalp t by ord_tac.
move: (ord_succ_lt oa)=> lt1.
move /(Schutte_Cr_p6 oa ot):(eq) => [y oy yb].
have : Schutte_phi a t <o x.
apply/(Schutte_phi_p7 ot OS0 oa (OS_succ oa)); split => //.
by move => e2; move: (proj2 lt1); rewrite - e2.
move => [h]; ord_tac.
rewrite eq yb /x => eq2.
case (ord_zero_dichot oy) => yz; first by move: (proj2 eq2); rewrite yz.
move: (proj1 (proj1 (Schutte_phi_p1 (OS_succ oa)) _ _ yz)) => h; ord_tac.
have pd: forall t, t<o x -> Schutte_phi a t = Schutte_psi a t.
move => t tx.
rewrite /Schutte_psi; Ytac H => //.
move: H => [n [c [on oc tv eq]]].
have cx: c<o x.
apply: ord_le_ltT tx; rewrite tv; apply: osum_Mle0=> //; ord_tac.
by case (pc _ cx).
have: \osup (fun_image x (Schutte_phi a)) = \osup (fun_image x (Schutte_psi a)).
by apply: ord_sup_2funI => t tx; apply: pd; apply /ord_ltP.
rewrite - (pb _ limx) - (pb' _ limx).
move: (Schutte_phi_p3 OS0 (ord_succ_lt oa)); rewrite -/x => -> h.
by move:(proj2 (Schutte_psi_p2 oa ox)); rewrite - h.
Qed.

Lemma Schutte_psi_limit a b: ordinalp a -> ordinalp b ->
(a <> \0o \/ b <> \0o) -> limit_ordinal (Schutte_psi a b).
Proof.
move => oa ob ha.
have:Schutte_psi a b <> \1o.
move:(Schutte_psi_p0 OS0);rewrite (Schutte_phi_p0 OS0) (opowx0) => <-.
by move/(Schutte_psi_p4 oa OS0 ob OS0) => [sa sb];case: ha.
rewrite /Schutte_psi; set c := Yo _ _ _.
have oc: ordinalp c by rewrite /c; Ytac h; fprops.
case: (indecomp_limit(Schutte_Cr_p8' oa oc)) => //.
Qed.

Lemma Schutte_psi_p11 x y : ordinalp x -> ordinalp y ->
Schutte_psi x y <=o Schutte_phi x (succ_o y).
Proof.
move => ox oy;rewrite /Schutte_psi; Ytac h3.
apply: ord_leR; apply:OS_Schutte_phi; fprops.
by move:((proj1 (Schutte_phi_p1 ox) _ _ (ord_succ_lt oy))) => [].
Qed.

Lemma Schutte_psi_p12 i j x y :
ordinalp i -> ordinalp j -> ordinalp x -> ordinalp y ->
(Schutte_psi i x <o Schutte_psi j y <->
[/\ i <o j -> x <o Schutte_psi j y,
i = j -> x <o y &
j <o i -> Schutte_psi i x <=o y]).
Proof.
move => oi oj ox oy.
have aux: forall i' j' x' y', i' <o j' -> ordinalp x' -> ordinalp y' ->
x' <o Schutte_psi j' y' -> Schutte_psi i' x' <o Schutte_psi j' y'.
move => i' j' x' y' pa ox' oy' sa.
move: (pa) => [[oi' oj' _] _].
have: limit_ordinal (Schutte_psi j' y').
apply:(Schutte_psi_limit oj' oy'); left; ord_tac1.
move/(limit_ordinal_P3) => [_ h1]; move: (h1 _ sa) => h2.
have ha:= (Schutte_psi_p11 oi' ox').
move: (ord_le_ltT ha ((proj1 (Schutte_phi_p1 oi') _ _ h2))).
rewrite {2 4} /Schutte_psi; set c := Yo _ _ _.
have oc: ordinalp c by rewrite /c; Ytac h4; fprops.
by rewrite (Schutte_phi_p3 oc pa).
case (ord_le_to_ell oi oj) => ij.
- have bad: i <o i -> False by move => [].
rewrite - ij; split.
move => h; split => h1; try (by case: bad).
case: (ord_le_to_ell ox oy) => // h2.
by move: (proj2 h); rewrite h2.
move: (proj1 (Schutte_psi_p3 oi h2)) => h3; ord_tac.
move => [_ h _]; exact: (Schutte_psi_p3 oi (h (erefl i))).
- split.
move => h; split.
+ move => _; case (ord_le_to_el (OS_Schutte_psi oj oy) ox) => // h1.
move: (ord_le_ltT (proj1 (Schutte_psi_p2 oi ox)) h) => h2; ord_tac.
+ by move => eq; move: (proj2 ij); case.
+ move=> [eq _]; ord_tac.
by move => [h _ _]; move: (h ij) => sa; by apply: aux.
- split.
move => h; split.
+ move=> [eq _]; ord_tac.
+ by move => eq; move: (proj2 ij); case.
+ move => _.
case (ord_le_to_el (OS_Schutte_psi oi ox) oy) => // h1.
move:(proj1 (aux _ _ _ _ ij oy ox h1)) => h2; ord_tac.
move => [_ _ h]; move: (h ij) => sa.
move: (Schutte_psi_p2 oj oy) => h2; ord_tac.
Qed.

CNF below Gamma0 via psi

Definition CNF_from_psi (a b: fterm) z := olog (Schutte_psi (a z) (b z)).

Definition CNF_psi_ax a b n :=
(forall i, i <c n -> ordinalp (a i) /\ (ordinalp (b i))) /\
(forall i, inc i Bnat -> succ i <c n ->
Schutte_psi (a i) (b i) <=o
Schutte_psi (a (succ i)) (b (succ i))).

Definition CNF_psi_ax2 a b n :=
CNF_psi_ax a b n /\
(forall i, i <c n -> (a i) <o Gamma_0 /\ (b i) <o Gamma_0).

Definition CNF_psiv a b n :=CNFrv0 (CNF_from_psi a b) n.

Lemma CNF_psi_p0 a b n: CNF_psi_ax a b n -> inc n Bnat ->
CNF_psiv a b n =
osum_expansion (fun i => (Schutte_psi (a i) (b i))) n.
Proof.
move => [a1 a2] nB.
apply: (osum_expansion_exten nB) => i lin.
move: (a1 _ lin) => [pb pc];exact (proj2 (ologp_psi pb pc)).
Qed.

Lemma CNF_psi_p1 a b n: CNF_psi_ax a b n -> CNFr_ax0 (CNF_from_psi a b) n.
Proof.
move => [ax1 ax2]; split.
move => i lin; move: (ax1 _ lin) => [qa qb].
exact (proj1 (ologp_psi qa qb)).
move => i iB lin.
move: (ax1 _ (card_le_ltT (card_le_succ iB) lin)) => [qc qd].
move: (ax1 _ lin) => [qa qb]; rewrite /CNF_from_psi.
move: (proj2 (ologp_psi qa qb)) (proj2 (ologp_psi qc qd)) => eq1 eq2.
move:(ax2 i iB lin). rewrite -{1} eq1 - {1} eq2 => h.
move: (ologp_psi qa qb) (ologp_psi qc qd) =>[r1 r2][r3 r4].
case: (ord_le_to_el r3 r1) => // /opow_Momega_lt h'; ord_tac.
Qed.

Lemma CNF_psi_unique a1 b1 n a2 b2 m:
inc n Bnat -> inc m Bnat -> CNF_psi_ax a1 b1 n -> CNF_psi_ax a2 b2 m ->
CNF_psiv a1 b1 n = CNF_psiv a2 b2 m ->
[/\ n = m, same_below a1 a2 n & same_below b1 b2 m].
Proof.
move => nB mB sa sb sc.
move: (CNFr_unique1 (CNF_psi_p1 sa) (CNF_psi_p1 sb) nB mB sc) => [sd se].
have aux: forall i, i<c n -> (a1 i = a2 i /\ b1 i = b2 i).
move => i lin.
move: (lin); rewrite sd => lim.
move: (proj1 sa _ lin) (proj1 sb _ lim) => [o1 o2] [o3 o4].
apply: (Schutte_psi_p4 o1 o3 o2 o4).
move:(ologp_psi o1 o2)(ologp_psi o3 o4)=> [_ <- ][_ <-].
by rewrite-/(CNF_from_psi _ _ _) -/(CNF_from_psi _ _ _) (se _ lin).
by hnf; rewrite - sd; split; first exact; move => i /aux [].
Qed.

Lemma CNF_psi_exists x: ordinalp x ->
exists a b n, [/\ inc n Bnat, CNF_psi_ax a b n & x = CNF_psiv a b n].
Proof.
move => ox; move:(CNFr_exists ox) => [f pa pb].
pose fa i := P (inv_psi_omega (Vg f i)).
pose fb i := Q (inv_psi_omega (Vg f i)).
set n := cardinal (domain f).
move: pa => [p1 p2 p3].
move: (CNF_domain1 p1) => nB.
have ha:forall i, i <c n -> ordinalp (fa i) /\ ordinalp (fb i).
move => i lin.
have hi: inc i (domain f) by apply/(CNF_domainP p1).
move:(inv_psi_omega_p (p2 _ hi)) => [_ [ha _ _] [[hb _ _] _] _].
by split.
have ax:CNF_psi_ax fa fb n.
split; [exact | move => i iB lin].
have lin':=(card_le_ltT (card_le_succ iB) lin).
have sid: inc (succ i) (domain f) by apply/(CNF_domainP p1).
have id: inc i (domain f) by apply/(CNF_domainP p1).
move: (p3 _ id sid) => sa.
move:(inv_psi_omega_p (proj31 sa)) => [_ _ _ ->].
move:(inv_psi_omega_p (proj32 sa)) => [_ _ _ ->].
by apply:opow_Momega_le.
exists fa, fb, n; split; [ exact | exact |].
rewrite pb; apply: (osum_expansion_exten nB) => i lin.
have id: inc i (domain f) by apply/(CNF_domainP p1).
rewrite /CNF_from_psi; move:(inv_psi_omega_p (p2 _ id)) => [_ _ _ ->].
by rewrite (ologp (p2 _ id)).
Qed.

Lemma CNF_psi_lt_Gamma0 a b n: inc n Bnat -> CNF_psi_ax2 a b n ->
CNF_psiv a b n <o Gamma_0.
Proof.
rewrite /CNF_psiv/CNFrv0.
have gl:= Gamma0_limit.
move: n; apply: cardinal_c_induction.
by move => _; rewrite osum_expansion0; move/limit_positive: gl.
move => n nB Hrec [[h1 h2] h3].
have nn:=(card_lt_succ nB).
move: (indecomp_prop4 (proj31 gl)); rewrite Gamma0_epsilon.
rewrite /CNF_psiv /CNFrv0 (osum_expansion_succ _ nB).
have: CNF_psi_ax2 a b n.
split; first split.
+ move => i lin; apply: h1; co_tac.
+ move => i iB slin; apply: h2 => //; co_tac.
+ move => i lin; apply:h3 => //; co_tac.
move /Hrec; apply: indecomp_prop2.
move: (h3 _ nn) => [sa sb].
move: (Gamma0_s_psi sa sb). rewrite /CNF_from_psi.
by rewrite (proj2(ologp_psi (proj31_1 sa) (proj31_1 sb))).
Qed.

Lemma CNF_psi_exists_Gamma0 x: x <o Gamma_0 ->
exists a b n, [/\ inc n Bnat, CNF_psi_ax2 a b n & x = CNF_psiv a b n].
Proof.
move => h; move: (CNF_psi_exists (proj31_1 h)) => [a [b [n [nB pb xv]]]].
exists a,b,n => //; split => //; split; first by exact.
move => i idf.
move: (CNFr_p3 nB (CNF_psi_p1 pb) idf).
rewrite /CNF_from_psi.
move:(proj1 pb _ idf) => [pd pe].
move:(ologp_psi pd pe) => [_ ->].
rewrite -/(CNF_psiv a b n) - xv => l1; move: (ord_le_ltT l1 h) => ha.
split.
exact: (ord_le_ltT (Schutte_psi_p2' pd pe) ha).
exact: (ord_le_ltT (proj1 (Schutte_psi_p2 pd pe)) ha).
Qed.

## Initial ordinals

Lemma iclosed_non_coll_infinite_c:
(iclosed_collection infinite_c) /\ non_coll (infinite_c).
Proof.
have H: ordinal_prop infinite_c by move => x [[oc _]_].
split; first split => //.
move => F iF [y yF].
have cs: cardinal_set F by move => z /iF [].
exact (ge_infinite_infinite (iF _ yF) (card_sup_ub cs yF)).
apply: unbounded_non_coll => //.
move => x ox; case: (ord_le_to_ee ox OS_omega) => cxo.
exists omega0 => //; apply: omega_infinitec.
have aux: cardinal x <c \2c ^c x by rewrite - cpow_prb; apply: cantor; fprops.
move: (ge_infinite_infinite (infinite_set_pr3 cxo) (proj1 aux)) => aux2.
move /(ordinal_cardinal_le2P (proj1 aux2) ox): aux => [aux3 _].
by exists (\2c ^c x).
Qed.

Definition omega_fct := ordinalsf (infinite_c).
Definition ord_index:=
ordinalr (fun x y => [/\ infinite_c x, infinite_c y & x <=o y]).

Notation "\omega" := omega_fct.
Notation "\aleph" := omega_fct (only parsing).
Definition omega1 := \omega \1o.
Definition aleph1 := \aleph \1o.
Definition omega2 := \omega \2o.
Definition aleph2 := \aleph \2o.
Definition aleph0 := omega0.

Lemma aleph_pr11: normal_ofs \omega.
Proof.
by move: iclosed_non_coll_infinite_c => [pa pb];apply:ordinals_col_p2.
Qed.

Lemma aleph_pr1: \omega \0o = omega0.
Proof.
move: iclosed_non_coll_infinite_c => [pa pb].
move: (iclosed_col_f0 pa pb) => [pc pd].
move: (pd _ omega_infinitec) (omega_limit3 pc)=> [_ _ sa] sb.
by apply: extensionality.
Qed.

Lemma succ_c_pr n: ordinalp n ->
succ_c (\aleph n) = \aleph (succ_o n).
Proof.
move: iclosed_non_coll_infinite_c => [pa pb] on.
move: (iclosed_col_fs pa pb on).
move => [xy icx icy h]; move: (icx)(icy) => [cx _] [cy _].
move: (succ_c_pr1 cx)=> [ua ub uc]; apply: card_leA.
apply: uc; apply:(ordinal_cardinal_lt3 cx cy xy).
move: (ge_infinite_infinite icx (proj1 ub)) => sa.
move: (h _ sa (ordinal_cardinal_lt ub)).
apply:(ordinal_cardinal_le3 cy ua).
Qed.

Lemma aleph_pr5c x: ordinalp x -> infinite_c (\aleph x).
Proof.
move: iclosed_non_coll_infinite_c => [ [pa _] pb].
move:(ordinals_col_p1 pa pb) => [h _ _ _ _].
apply: h.
Qed.

Lemma CS_aleph x: ordinalp x -> cardinalp (\aleph x).
Proof. by move=> /aleph_pr5c []. Qed.

Hint Resolve CS_aleph: fprops.

Lemma OS_aleph x: ordinalp x -> ordinalp (\omega x).
Proof. by move=> /CS_aleph []. Qed.

Lemma aleph_pr5 x: ordinalp x -> omega0 <=o (\omega x).
Proof. by move => /aleph_pr5c /infinite_c_P2 /ordinal_cardinal_le. Qed.

Lemma aleph_lt_lto x y: x <o y -> (\omega x) <o (\omega y).
Proof. apply (proj1 aleph_pr11). Qed.

Lemma aleph_le_leo x y: x <=o y -> (\omega x) <=o (\omega y).
Proof.
move => xy; case: (equal_or_not x y) => nxy.
rewrite - nxy.
move: (OS_aleph (proj31 xy)) => aux; ord_tac.
by move: (aleph_lt_lto (conj xy nxy)) => [ok _].
Qed.

Lemma aleph_leo_le x y: ordinalp x -> ordinalp y ->
(\omega x) <=o (\omega y) -> x <=o y.
Proof.
move=> oa ob lef.
case: (ord_le_to_el oa ob) => //.
move=> aux; move: (aleph_lt_lto aux) => aux2; ord_tac.
Qed.

Lemma aleph_eq x y: ordinalp x -> ordinalp y ->
(\omega x) = (\omega y) -> x = y.
Proof.
move=> oa ob lef.
by case: (ord_le_to_ell oa ob) => // /aleph_lt_lto []; rewrite lef.
Qed.

Lemma aleph_lto_lt x y: ordinalp x -> ordinalp y ->
(\omega x) <o (\omega y) -> x <o y.
Proof.
move => ox oy lt1.
case: (ord_le_to_el oy ox) => // h.
move: (aleph_le_leo h) => h1; ord_tac.
Qed.

Lemma aleph_pr6 x: ordinalp x -> x <=o (\omega x).
Proof. apply: (osi_gex aleph_lt_lto). Qed.

Lemma aleph_le_lec x y: x <=o y -> \aleph x <=c \aleph y.
Proof.
move=> xy; move: (xy) => [ox oy _].
by apply /ordinal_cardinal_le3; fprops; apply:aleph_le_leo.
Qed.

Lemma aleph_lt_ltc x y: x <o y -> \aleph x <c \aleph y.
Proof.
move=> xy; move: (xy) => [[ox oy _] _].
by apply /ordinal_cardinal_lt3; fprops; apply:aleph_lt_lto.
Qed.

Lemma aleph_lec_le x y: ordinalp x -> ordinalp y ->
(\aleph x) <=c (\aleph y) -> x <=o y.
Proof.
by move => h h1 h2; apply: aleph_leo_le => //; apply:ordinal_cardinal_le.
Qed.

Lemma aleph_ltc_lt x y: ordinalp x -> ordinalp y ->
(\aleph x) <c (\aleph y) -> x <o y.
Proof.
by move => h h1 h2; apply: aleph_lto_lt => //; apply:ordinal_cardinal_lt.
Qed.

Lemma aleph_nz x: ordinalp x -> \aleph x <> \0c.
Proof.
move=> ox;move: (aleph_pr5c ox) => ix vx.
rewrite vx in ix;case: (infinite_dichot1 finite_zero ix).
Qed.

Lemma aleph_nz1 x: ordinalp x -> \0c <c \aleph x.
Proof.
move=> ox; split; first by apply: czero_least; apply: CS_aleph.
by move =>h;case: (aleph_nz ox).
Qed.

Lemma ord_index_pr1 x: infinite_c x ->
(ordinalp (ord_index x) /\ \aleph (ord_index x) = x).
Proof. by move =>icx; apply: ordinalrsP => // t [[]]. Qed.

Lemma ord_index_pr n: ordinalp n ->
ord_index (\aleph n) = n.
Proof.
move => on; move: (aleph_pr5c on) => pc.
move: (ord_index_pr1 pc); move => [h1 h2].
exact: (aleph_eq h1 on h2).
Qed.

Definition ContHypothesis:= succ_c omega0 = \2c ^c omega0.
Definition GenContHypothesis:= forall x, infinite_c x -> succ_c x = \2c ^c x.

Lemma aleph_pr10a x y: ordinalp x ->
y <c \aleph (succ_o x) -> y <=c \aleph x.
Proof.
move => ox lt1; move: (lt1) => [[cy cso _] _].
case: (card_le_to_el cy (CS_aleph ox)) => // pc.
have iy := (ge_infinite_infinite (aleph_pr5c ox) (proj1 pc)).
move: (ord_index_pr1 iy) lt1 => [ox' <- /(aleph_ltc_lt ox' (OS_succ ox))].
by move /ord_lt_succP/aleph_le_lec.
Qed.

Lemma aleph_pr10b x y: ordinalp x ->
\aleph x <c y -> \aleph (succ_o x) <=c y.
Proof.
move=> ox h.
have cy: cardinalp (\aleph (succ_o x)) by apply: CS_aleph; fprops.
case: (card_le_to_el cy (proj32_1 h)) => // pc.
move: (aleph_pr10a ox pc) => aux; co_tac.
Qed.

Lemma aleph_pr10c x: ordinalp x ->
\aleph x <c \aleph (succ_o x).
Proof. by move=> ox; apply: (aleph_lt_ltc); apply: ord_succ_lt. Qed.

Lemma Cantor_omega_pr3: aleph1 = aleph_one.
Proof. by rewrite /aleph1 - succ_o_zero - (succ_c_pr OS0) aleph_pr1. Qed.

Lemma aleph_limit x: ordinalp x -> limit_ordinal (\omega x).
Proof. by move => ox; apply: infinite_card_limit2; apply: aleph_pr5c. Qed.

Lemma aleph_pr12b x z :
ordinalp x -> ordinalp z -> \aleph x <c cardinal z ->
\aleph (succ_o x) <=o z.
Proof.
move=> ox oz ycz.
move: (cardinal_ordinal_le oz) => le1.
have osx: ordinalp (succ_o x) by fprops.
move: (ordinal_cardinal_le (aleph_pr10b ox ycz)) => le2; ord_tac.
Qed.

Lemma aleph_pr12c x z:
ordinalp x -> ordinalp z -> cardinal z <=c \aleph x ->
z <o \aleph (succ_o x).
Proof.
move=> ox oz p1; move: (p1) => [_ cy _].
rewrite - (succ_c_pr ox); apply /(ord_ltP (proj1 (CS_succ_c cy))).
by apply/succ_cP.
Qed.

Lemma aleph_pr12d x z:
ordinalp x -> z <o (\aleph (succ_o x)) ->
cardinal z <=c (\aleph x).
Proof.
move => ox lt1.
have oz: ordinalp z by ord_tac.
have cz: cardinalp (cardinal z) by fprops.
case: (card_le_to_el cz (CS_aleph ox)) => // h.
move: (aleph_pr12b ox oz h) => h'; ord_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 aleph_pr12e x: ordinalp x ->
\aleph (succ_o x) <c \2c ^c (\2c ^c (\aleph x)).
Proof.
move => ocx;move: (aleph_pr5c ocx); set E:= \aleph x => ife.
suff: \omega (succ_o x) <=c (\2c ^c E).
move => h; apply: (card_le_ltT h); apply: (cantor (proj32 h)).
rewrite - (succ_c_pr ocx); apply:succ_c_pr3; apply:(CS_aleph ocx).
Qed.

## cardinal cofinality

Definition csum_of_small0 x f:=
fgraph f /\ allf f (fun z => z <=c x).
Definition csum_of_small1 x f:=
fgraph f /\ allf f (fun z => z <c x).

Lemma csum_commutative1 f x:
csum_of_small1 x f -> exists g,
[/\ csum_of_small1 x g, domain g = (cardinal (domain f)),
card_sum f = card_sum g & range g = range f].
Proof.
move=> [fgf pb].
move: (CS_cardinal (domain f)) => [ocy cyp].
set z1 := cardinal (domain f).
have [g [bg sg tg]]: z1 \Eq (domain f) by rewrite /z1; fprops.
set h := Lg z1 (fun i => Vg f (Vf g i)).
have dh: domain h = z1 by rewrite /h; bw.
have fgh: fgraph h by rewrite /h; fprops.
have sh: forall i, inc i (domain h) -> Vg h i <c x.
rewrite /h; bw => i id; bw; apply: pb.
rewrite - tg; apply: Vf_target; try fct_tac; ue.
have ch: cardinal_fam h by move => a ay; move: (sh _ ay) => lt; co_tac.
have fg: function g by fct_tac.
have rh: range h = range f.
rewrite /h; set_extens t.
move/(range_gP fgh); rewrite dh; move => [u p1 ->]; rewrite /h; bw.
apply /(range_gP fgf); exists (Vf g u)=> //; rewrite -tg; Wtac.
move /(range_gP fgf) => [u p1 ->]; apply/(range_gP fgh).
rewrite - tg in p1; move: ((bij_surj bg) _ p1) => [w usg ww].
rewrite /h; rewrite dh - sg; ex_tac; bw; ue.
exists h => //; split => //.
have ->: h = f \cf (graph g).
rewrite /composef /h /Vf.
have -> //: domain (graph g) = z1 by rewrite f_domain_graph //.
apply: csum_Cn => //.
Qed.

Lemma csum_of_small_b1 x f: csum_of_small0 x f ->
card_sum f <=c (x *c (domain f)).
Proof.
move=> [p1 p2];rewrite - csum_of_same.
by apply:csum_increasing; bw => //; fprops => a adf; bw; apply: p2.
Qed.

Lemma csum_of_small_b2 x f: csum_of_small1 x f ->
card_sum f <=c (x *c (domain f)).
Proof.
by move=> [p1 p2]; apply: (csum_of_small_b1); split => // i /p2 [].
Qed.

Lemma csum_of_small_b3 x f:
csum_of_small1 x f ->
(exists2 n, ordinalp n & x = \aleph (succ_o n)) ->
(cardinal (domain f)) <c x -> (card_sum f) <c x.
Proof.
move=> [pa pb] [n on xv] zx.
rewrite xv in zx.
move: (aleph_pr10a on zx) => le1.
have pe: (allf f (cardinal_le ^~ (\omega n))).
move=> i /pb; rewrite xv; apply: (aleph_pr10a on).
move: (csum_of_small_b1 (conj pa pe)) => le2.
move: (product2_infinite1 le1 (aleph_pr5c on)); rewrite cprod2_pr2b => le3.
rewrite xv; exact (card_le_ltT (card_leT le2 le3) (aleph_pr10c on)).
Qed.

Lemma csum_of_small_b4 f (s:= \csup (range f)) :
fgraph f -> cardinal_fam f -> infinite_c s ->
(cardinal (domain f) <=c s) -> card_sum f = s.
Proof.
move=> pa1 pa pb pc.
have csr: cardinal_set (range f).
by move=> t /(range_gP pa1) [u ua ->]; apply: pa.
have pe: s *c domain f = s.
rewrite - cprod2_pr2b; apply: product2_infinite => //.
apply: cardinal_nonemptyset1.
case: (emptyset_dichot (domain f)) => // de.
move: (finite_lt_infinite finite_0 pb) => [_]; rewrite /s.
have -> :(range f = emptyset) by apply /range_set0_P; apply/domain_set0_P.
by rewrite setU_0;case.
apply: card_leA.
have pd: (allf f (cardinal_le ^~ s)).
move=> i idf; apply: (card_sup_ub csr); apply /(range_gP pa1); ex_tac.
by rewrite - pe; apply:(csum_of_small_b1 (conj pa1 pd)).
apply: card_ub_sup => //; first by rewrite /card_sum; fprops.
move => a /(range_gP pa1) [x xdf ->]; apply: csum_increasing6 => //.
Qed.

Lemma csum_of_small_b5 f (s:= \csup (range f)) :
fgraph f -> cardinal_fam f ->
(exists i, [/\ inc i (range f), infinite_c i & cardinal (domain f) <=c i])
-> card_sum f = s.
Proof.
move => pa pa2 [i [ir l1 l2]].
have csr: cardinal_set (range f)
by move=> t /(range_gP pa) [u ua ->]; apply: pa2.
move: (card_sup_ub csr ir) => pb.
apply: csum_of_small_b4 => //; [apply: (ge_infinite_infinite l1 pb) | co_tac].
Qed.

Definition cofinality_c_ex x z :=
exists f, [/\ csum_of_small1 x f, domain f = z & card_sum f = x].
Definition cofinality_c x:=
least_ordinal (cofinality_c_ex x) x.
Definition regular_cardinal x :=
infinite_c x /\ cofinality_c x = x.

Lemma cofinality_c_rw x (y:= cofinality_c x): \2c <=c x ->
[/\ y <=c x,
cofinality_c_ex x y
& (forall z, ordinalp z -> (cofinality_c_ex x z) -> y <=o z)].
Proof.
move=> x2.
have cx: cardinalp x by co_tac.
move: (cx) => [ox _].
have x1: \1c <c x by move: card_lt_12 => aux; co_tac.
pose p := cofinality_c_ex x.
have px: p x.
exists (cst_graph x \1c); split.
- split;[ fprops | hnf; bw=> a ax; bw].
- bw.
- by move: (csum_of_ones x); rewrite /cst_graph => ->; apply: card_card.
move: (least_ordinal1 ox px) => [].
rewrite -/(cofinality_c x) -/y; move=> oy py pb.
have pa: forall z, ordinalp z -> p z -> y <=o z.
by move => z oz pz; move: (pb _ oz pz)=> yz.
split => //.
move: py => [f [qa qb qc]].
move: (csum_commutative1 qa)=> [g [ga gb gc gd]].
have pcy: p (cardinal y) by exists g; rewrite gb qb - gc qc.
move: (CS_cardinal y) => [ocy cyp].
move: (pb _ ocy pcy) => hh.
move: (extensionality (cyp _ oy (cardinal_pr y)) hh) => H.
split => //; [ rewrite - H; fprops | exact: (pb _ ox px)].
Qed.

Lemma cofinality_c_pr2 x: \2c <=c x ->
exists f, [/\ csum_of_small1 x f, domain f = (cofinality_c x), card_sum f = x
& (allf f (fun z => z <> \0c)) ].
Proof.
move=> h; move: (cofinality_c_rw h) => [pa pb pc].
move: pb => [f [[pd pe] pf pg]].
set j := Zo (domain f) (fun z => Vg f z <> \0c).
have sj: sub j (domain f) by apply: Zo_S.
have qa: (forall i, inc i ((domain f) -s j) -> Vg f i = \0c).
move=> i /setC_P [r1] /Zo_P r2; ex_middle h0; case: r2; split => //.
move: (csum_zero_unit sj qa) => h1; rewrite h1 in pg.
have h2: csum_of_small1 x (Lg j (Vg f)).
split; [ fprops | by hnf; bw;move=> a ad; bw; apply: pe; apply: sj].
move: (csum_commutative1 h2) => [g []]; bw => ga gb gc gd.
have xsg: card_sum g = x by rewrite - gc.
set z := (cardinal j).
have oz: ordinalp z by apply: OS_cardinal; apply: CS_cardinal.
have h3: cofinality_c_ex x z by exists g.
move: (pc _ oz h3) => le2.
have le3: z <=c cofinality_c x.
move : (sub_smaller sj); rewrite pf -/z card_card //; co_tac.
have ->: cofinality_c x = z by move: (ordinal_cardinal_le le3) => le4; ord_tac.
exists g; split => //.
have : inc \0c (range (Lg j (Vg f))).
rewrite - gd;apply/(range_gP (proj1 ga)); ex_tac.
rewrite Lg_range => /funI_P [u uj].
by move: uj => /Zo_hi pdd pw; case: pdd.
Qed.

Lemma cofinality_c_pr3 x: infinite_c x ->
exists f, [/\ csum_of_small1 x f, domain f = (cofinality_c x), card_sum f = x
& (allf f (fun z => \2c <=c z)) ].
Proof.
move => icx; move: (infinite_ge_two icx) => x1.
move: (cofinality_c_rw x1) => [pa pb pc].
move: pb => [f [[pd1 pd2] pe pf]].
move: (sum_of_sums (Vg f) (fun _:Set => \2c) (domain f)).
rewrite /card_sumb (Lg_recovers pd1) csum_of_same pf pe.
have ->: x +c \2c *c cofinality_c x = x.
move: (sum2_infinite pa icx) => xx.
by rewrite two_times_n csumA xx xx.
move=> xv.
exists (Lg (cofinality_c x) (fun i => Vg f i +c \2c)); split.
- split; [ fprops | hnf; bw => i idf; bw].
rewrite -pe in idf;move: (pd2 _ idf) => lt1.
apply:csum_lt_infinite => //; apply: (finite_lt_infinite finite_2 icx).
- bw.
- done.
- hnf; bw; move=> i ic; bw; rewrite csumC ;apply: csum_M0le; fprops.
Qed.

Lemma cofinality_c_small x: \2c <=c x -> (cofinality_c x) <=c x.
Proof. by move=> x1; move: (cofinality_c_rw x1) => [ok _]. Qed.

Lemma CS_cofinality_c x: \2c <=c x ->
cardinalp (cofinality_c x).
Proof. by move=> x1; move: (cofinality_c_small x1) => [ok _]. Qed.

Lemma cofinality_c_finite x: \2c <=c x -> finite_c x ->
cofinality_c x = \2c.
Proof.
move=> x1 fcx.
move: (cofinality_c_rw x1) => [p3 p4 p5].
set y:= cofinality_c x.
have xnz: x <> \0o.
move => xz; rewrite xz in x1; move:card_lt_02 => auc; co_tac.
move: p4 => [f [[q1 q2] df q3]].
case: (ord2_trichotomy (proj1 (proj31 p3))) => h.
have dfe: domain f = emptyset by rewrite df h.
by case: xnz; rewrite -q3 (csum_trivial dfe).
have df1: domain f = singleton \0c by rewrite df h.
have zc: inc \0c (domain f) by rewrite df1; fprops.
move: (q2 _ zc); rewrite -q3 (csum_trivial2 df1); move =>[le1].
rewrite card_card //; co_tac.
apply: (ord_leA) => //; apply: p5; first by apply: OS2.
have xB: inc x Bnat by apply /BnatP.
move: (cpred_pr xB xnz) => []; set p:= cpred x; move => p4 p5.
have lpx: p <c x by rewrite p5; apply: card_lt_succ.
have cp: cardinalp p by fprops.
symmetry in p5; move: p5; rewrite (card_succ_pr4 cp).
set g:= (variantL \0c \1c p \1c).
have dg : \2c = domain g by rewrite /g/variantL; bw.
have fgg: fgraph g by rewrite /g/variantL; fprops.
have q4': doubleton_fam g p \1c.
exists \0c; exists \1c; split;fprops; rewrite /g.
by rewrite variant_V_a.
rewrite variant_V_b //; fprops.
rewrite (csum2_pr q4') => p5.
have p6: forall i, inc i (domain g) -> Vg g i <c x.
have aux: \1c <c x by move: card_lt_12 => aux; co_tac.
move => i; rewrite /g {1} /variantL; bw; case /set2_P => ->; bw.
exists g;split => //;split => //; split => //.
Qed.

Lemma cofinality_infinite x: infinite_c x -> infinite_c (cofinality_c x).
Proof.
move=> icx; move: (infinite_ge_two icx) => x1.
move: (cofinality_c_rw x1) => [pc pd pe].
have cs: cardinalp (cofinality_c x) by co_tac.
case: (finite_dichot cs) => // cf.
move: (cf); rewrite - (card_card cs) -/(finite_set _) => fs.
move: pd => [f [[fa fb] fc fd]].
set E := fun_image (domain f) (fun z => Vg f z).
have fe: finite_set E by apply: finite_fun_image; ue.
have nee: nonempty E.
case: (emptyset_dichot (domain f)) => de.
move: (csum_trivial de); rewrite fd => h.
move: card_lt_02 => aux; rewrite h in x1; co_tac.
move: de => [i ie]; exists (Vg f i); apply /funI_P; ex_tac.
have cse: cardinal_set E.
move=> t /funI_P [z zdf ->]; move: (fb _ zdf)=> h; co_tac.
move: (wordering_cardinal_le_pr cse) => [qa qb].
move: (finite_set_torder_greatest (worder_total qa)); rewrite qb => aux.
move: (aux fe nee)=> [t []]; rewrite qb => qc qd.
have tx: t <c x by move: qc => /funI_P [z0 /fb zd ->].
have tx1: (allf f (cardinal_le^~ t)).
move=> i idf; have vE: inc (Vg f i) E by apply /funI_P; ex_tac.
by move: (qd _ vE) => /graph_on_P1 [_ _].
move: (csum_of_small_b1 (conj fa tx1)); rewrite fc => sc.
have ct: cardinalp t by co_tac.
case: (finite_dichot ct) => // fct.
have fp: finite_c (t *c cofinality_c x).
by apply /BnatP; apply: BS_prod; apply/BnatP.
move: (finite_lt_infinite fp icx). rewrite - {2} fd=> sa; co_tac.
move: (finite_lt_infinite cf fct) => [le1 _].
move: (product2_infinite1 le1 fct) => sb.
move: (card_leT sc sb); rewrite fd => sd; co_tac.
Qed.

Lemma infinite_regularP x: infinite_c x ->
(regular_cardinal x <->
forall f, csum_of_small1 x f -> cardinal (domain f) <c x -> card_sum f <c x).
Proof.
move => ix.
have ox: ordinalp x by move: ix => [[ok _] _].
have x2: \2c <=c x by apply: infinite_ge_two.
move: (cofinality_c_rw x2) => [p3 [f [f1 f2 f3] p5]].
have cc: cardinalp (cofinality_c x) by co_tac.
split => h; last first.
move: (h f f1); rewrite f2 (card_card cc) => w;split => //;ex_middle bad.
by move: (w (conj p3 bad)) => [_]; rewrite f3.
move: h=> [_ rx] g gp [le1 ba].
move: (csum_commutative1 gp) => [h [h1 h2 h3 h4]].
split.
move: (csum_of_small_b2 h1); rewrite - h3 h2 => p6.
move: (product2_infinite1 le1 ix) => le2; co_tac.
move => cs; rewrite cs in h3; case: ba; apply: ord_leA.
by move: (ordinal_cardinal_le le1).
rewrite - rx; apply: p5; [ by apply: OS_cardinal; fprops | by exists h].
Qed.

Lemma regular_cardinal_omega: regular_cardinal omega0.
Proof.
move: omega_infinitec => ico; split => //.
move: (cofinality_c_small (infinite_ge_two ico)) => [_ _ pa].
move: (omega_limit3 (cofinality_infinite ico)) => pb.
by apply: extensionality.
Qed.

Lemma regular_initial_successor x: ordinalp x ->
regular_cardinal (\aleph (succ_o x)).
Proof.
move => ox.
have osx: ordinalp (succ_o x) by fprops.
move: (aleph_pr5c osx) => iy.
move: (infinite_ge_two iy) => y2.
move: (cofinality_c_rw y2) => [pc [f [fa fb fc] _]].
split => //; apply: (card_leA pc).
move: (pc);set X := \omega (succ_o x).
case: (equal_or_not (cofinality_c X) X) => eq; first by rewrite eq.
have en: (exists2 n, ordinalp n& X = \omega (succ_o n)) by exists x.
move: (csum_of_small_b3 fa en). rewrite fb (card_card (CS_cofinality_c y2)) fc.
by move => ha hb;move: (ha (conj hb eq)) => [_].
Qed.

Definition aleph_succ_comp x :=
(\aleph (succ_o x)) -s (\aleph x).

Lemma aleph_succ_P1 x: ordinalp x ->
(forall t, inc t (aleph_succ_comp x) <->
((\aleph x) <=o t /\ t <o (\aleph (succ_o x)))).
Proof.
move => ox t.
move: (aleph_lt_lto (ord_succ_lt ox)) => lt1.
move: (lt1) => [[oy oy' _] _].
split. move /setC_P => [ta tb].
have ot: ordinalp t by ord_tac.
split; last by apply /ord_ltP0;split => //.
by case: (ord_le_to_el oy ot) => //;move/ord_ltP0 => [_ _].
move => [[p1 p2 p3] p4]; apply /setC_P; split => //.
by move /(ord_ltP0) : p4 => [_ _].
move => p5; exact:(ordinal_irreflexive p2 (p3 _ p5)).
Qed.

Lemma aleph_succ_pr2 x: ordinalp x ->
cardinal (aleph_succ_comp x) = \aleph (succ_o x).
Proof.
move => ox.
move:(aleph_pr5c (OS_succ ox)) (aleph_lt_lto (ord_succ_lt ox)) => sa sb.
exact (proj2 (cardinal_indecomposable1 sa sb)).
Qed.

Lemma aleph_succ_pr3 x y: ordinalp x -> ordinalp y ->
x = y \/ disjoint (aleph_succ_comp x) (aleph_succ_comp y).
Proof.
move=> ox oy.
case: (equal_or_not x y); [by left | move => h0; right;apply /set0_P => t].
move /setI2_P => [] /(aleph_succ_P1 ox) [pa pb] /(aleph_succ_P1 oy) [pc pd].
case: h0; apply: ord_leA; apply /ord_lt_succP.
by move: (aleph_lto_lt ox (OS_succ oy) (ord_le_ltT pa pd)).
by move: (aleph_lto_lt oy (OS_succ ox) (ord_le_ltT pc pb)).
Qed.

Lemma aleph_sum_pr1 x: ordinalp x ->
inc x omega0 \/ exists2 y, ordinalp y & inc x (aleph_succ_comp y).
Proof.
move=> ox.
case: (normal_ofs_bounded ox aleph_pr11) => h.
by left; move: h; rewrite -aleph_pr1; move /ord_ltP0; move=> [_ _].
by move: h => [y [pa pb pc]]; right; exists y => //; apply /(aleph_succ_P1 pa).
Qed.

Lemma aleph_sum_pr2 x: ordinalp x ->
\aleph x = omega0 +c (card_sum (Lg x (fun z => \aleph (succ_o z)))).
Proof.
move=> ox.
have /cardinal_setC: sub omega0 (\aleph x).
by move: (aleph_pr5 ox) => [_ _].
rewrite (card_card (CS_aleph ox)) (card_card (CS_omega)).
move => <-; congr (_ +c _); rewrite /card_diff.
have oa := OS_aleph ox.
have ->: ((\aleph x) -s omega0) = unionb (Lg x aleph_succ_comp).
set_extens t.
move /setC_P;move=> [pa pb]. move: (ordinal_hi oa pa) => ot.
case: (aleph_sum_pr1 ot) => // [] [y oy ta].
move /(aleph_succ_P1 oy): (ta) => [pc pd].
suff yx: inc y x by apply /setUb_P; exists y; bw.
have le1: t <o (\aleph x) by apply /ord_ltP.
by move:(aleph_lto_lt oy ox (ord_le_ltT pc le1)) => /ord_ltP0[_ _].
move=> /setUb_P; bw; move => [y yx]; rewrite (LVg_E _ yx).
move/(ord_ltP ox): yx => yx.
have oy: ordinalp y by ord_tac.
move/(aleph_succ_P1 oy) => [p1 p2]; apply /setC_P; split.
move /ord_succ_ltP: yx => /(aleph_le_leo) ca.
by move: (ord_lt_leT p2 ca) => /ord_ltP0 [_ _].
move: (ord_leT (aleph_pr5 oy) p1) => [q1 q2 q3] q4.
exact: (ordinal_irreflexive q2 (q3 _ q4)).
apply /card_eqP;apply: equipotent_disjointU; last by fprops.
red; rewrite /disjointU_fam; split;fprops; bw.
move=> i ix; bw; eqtrans (\aleph (succ_o i)).
move: (ordinal_hi ox ix) => oi.
move: (CS_aleph (OS_succ oi)) => co.
by apply /card_eqP; rewrite (aleph_succ_pr2 oi) card_card.
red; bw; move=> i j ix jx; bw.
by apply: aleph_succ_pr3; apply: (ordinal_hi ox).
Qed.

Lemma aleph_sum_pr3 x: ordinalp x ->
\aleph x = card_sumb (succ_o x) \aleph.
Proof.
move=> ox.
set f:= (Lg (succ_o x) \aleph).
have fgf: fgraph f by rewrite /f; fprops.
have tdf: (x +s1 x) = (domain f) by rewrite /f; bw.
have sd: sub (x +s1 x) (domain f) by rewrite tdf; apply: sub_refl.
have ni: not (inc x x) by apply: (ordinal_irreflexive ox).
move: (induction_sum0 f ni); rewrite /card_sumb.
have ->: restr f (x +s1 x) = f by rewrite tdf restr_to_domain //.
move=> ->; rewrite {2} /f; bw; last by rewrite /succ_o; fprops.
suff: (card_sum (restr f x)) <=c (\aleph x).
move=> h; symmetry; rewrite csumC; apply: sum2_infinite => //.
by apply: aleph_pr5c.
rewrite (aleph_sum_pr2 ox).
set