proposition: Lemma Schutte_14_16 x: x <o Gamma_0 -> exists2 n, natp n & x <o Szeta n.
proof: Proof. move => h. pose p x :=x <o Gamma_0 -> exists2 n, natp n & x <o Szeta n. apply:(least_ordinal2 (p := p)) (proj31_1 h) h => y oy Hr yg. case (ozero_dichot oy). move => ->; exists \0o; first by apply:NS0. rewrite Szeta_0; apply:olt_01. move=> yp. move: (omega_log_p1 yp) => [z [oz pa pb]]. move: (Sphi_p10b (indecomp_prop4 oz)) => [a [b [az bz etc]]]. move: (proj31_1 bz) (proj31 az) => ob oa. have gp:=(proj2 Gamma0_p). have ag0:= (ole_ltT (oleT az pa) yg). have bg0:=(ole_ltT (oleT (proj1 bz) pa) yg). have az': a <o oopow z. split => //; rewrite etc => e1. case (ozero_dichot ob) => bez. have eq2: Sphi a \0o = a by rewrite - bez. exact: (oltNge ag0 (gp _ oa eq2)). move: (proj1 (Sphi_p1 oa) _ _ bez); rewrite - e1 => ga. case: (oltNge ga (osi_gex (proj1(Sphi_p5)) oa)). have lby:= (olt_leT bz pa). have lay:= (olt_leT az' pa). move: (Hr _ lby bg0) (Hr _ lay ag0)=> [n nN nb] [m mN ma]. set nm :=cmax n m. have nmN: natp nm by apply:Gmax_E. have laS: a <o Szeta nm. rewrite /nm/cmax/Gmax; Ytac w => //. case: (cleT_el (CS_nat nN) (CS_nat mN)) => // lmn. exact: (olt_ltT ma (Szeta_5 mN nN lmn)). have lbS: b <o Szeta nm. rewrite /nm/cmax/Gmax; Ytac w => //; case (equal_or_not n m) => ee; try ue. exact: (olt_ltT nb (Szeta_5 nN mN (conj w ee))). have lt1: oopow z <o Szeta (csucc nm). rewrite etc (Szeta_2 nmN). apply/(Sphi_p7 ob OS0 oa (proj32_1 laS)); split. + move: (Szeta_4 nmN); rewrite (Szeta_2 nmN). move => sa sb; exact: olt_ltT lbS sa. + by move => e1; move: (proj2 laS); rewrite - e1. + by move => [/(oltNge laS) e1 _]. exists (csucc nm); first by apply:NS_succ. have [u ou uv]: exists2 u, ordinalp u & Szeta (csucc nm) = omega0 ^o u. move: (proj32_1 laS) OS0 => o1 o2. by apply: indecomp_prop3;rewrite (Szeta_2 nmN); apply:Schutte_Cr_p8'. move: lt1; rewrite uv => hb. case: (oleT_el ou oz); first by move/opow_Mo_le => ha; case: (oleNgt ha hb). by move/(oleSltP) => /opow_Mo_le;apply: olt_leT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)