proposition: Lemma Gamma0_limit: limit_ordinal Gamma_0.
proof: Proof. have h:= (proj1 Gamma0_p). have og:= OS_Gamma_0. case:(indecomp_limit (Schutte_Cr_p8' og OS0)); rewrite h// => h2. move: h; rewrite h2 => h3. move: (Sphi_p3 OS0 (olt_01)). rewrite h3 (Sphi_p0 OS1) oopow1 => <-; exact omega_limit. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)