proposition: Lemma Schutte_14_16' x: x <o Gamma_0 -> exists2 n, natp n & x <o Szeta n.
proof: Proof. move => h; ex_middle bad. have ox:= (proj31_1 h). have: (forall n, natp n -> Szeta n <=o x). move => n nN; ex_middle b; case bad; exists n => //. case: (oleT_el (OS_Szeta nN) ox) => //. by move/(Szeta_6 ox) => /(oltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)