proposition: Lemma Spsi_limit a b: ordinalp a -> ordinalp b -> (a <> \0o \/ b <> \0o) -> limit_ordinal (Spsi a b).
proof: Proof. move => oa ob ha. have:Spsi a b <> \1o. move:(Spsi_p0 OS0);rewrite (Sphi_p0 OS0) oopow0 => <-. by move/(Spsi_p4 oa OS0 ob OS0) => [sa sb];case: ha. rewrite /Spsi; set c := Yo _ _ _. have oc: ordinalp c by rewrite /c; Ytac h; fprops. case: (indecomp_limit(Schutte_Cr_p8' oa oc)) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)