proposition: Lemma Spsi_p1 a b b': ordinalp a -> ordinalp b -> ordinalp b' -> (Spsi a b = Sphi a b') -> b' <o Sphi a b'.
proof: Proof. move => oa ob ob'; rewrite /Spsi => sa. have ica:= (proj1 (Sphi_p1 oa)). have pa:= (osi_gex ica ob). have oy: ordinalp (Yo (Spsi_aux a b) (osucc b) b) by Ytac h; fprops. move/(Sphi_p6 oy ob' oa oa): sa => [_ h _]; move: (h (erefl a)). Ytac h0 => eq2. move:(ole_ltT pa (ica _ _ (oltS ob)));rewrite -{1} eq2 {1} eq2. case:(indecomp_limit (Schutte_Cr_p8' oa ob')). move => -> /olt1 bz. move: h0 => [n [c [qa qb qc]]]. have cnz: c +o n = \0o by rewrite - bz. move: (osum2_zero qb (proj31_1 qa) cnz) => [-> _] e2. by move: (Schutte_Cr_p8' oa OS0) => [] []; rewrite e2 => _; case. move => /limit_ordinal_P [_]; apply. rewrite - eq2;split => // eq1; case h0; exists \0o, b; rewrite (osum0r ob). split => //;exact:olt_0omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)