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

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

Module Ordinals4.

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 => h; ex_middle bad.
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.