proposition: Lemma Szeta_6 x: ordinalp x -> (forall n, natp n -> Szeta n <=o x) -> Gamma_0 <=o x.
proof: Proof. move => ox pa. move: (induction_defined_pr (Sphi^~ \0o) \0o). rewrite /Gamma_0 /the_least_fixedpoint_ge. set f := induction_defined _ _. move => [sf sjf f0 fsn]. have f1: Vf f (csucc \0c) = Szeta \0o. by rewrite (fsn _ NS0) f0 - Szeta_1. have pb: forall n, natp n -> (Vf f (csucc n)) = Szeta n. apply: Nat_induction => // n nN hr. by rewrite (fsn _ (NS_succ nN)) hr (Szeta_2 nN). have aux: forall t, inc t (target f) -> t = \0o \/ (exists2 n, natp n & t = Szeta n). move => i /(proj2 sjf) [n]; rewrite sf => nN ->. case (equal_or_not n \0o) => nz; [by rewrite nz f0; left | right]. move: (cpred_pr nN nz) => [qa qb]; exists (cpred n) => //. by rewrite {1} qb pb. apply:ord_ub_sup => //. move => i /aux [-> | [n nb ->]]; [apply:ole0x ox | apply: pa nb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)