proposition: Lemma Spsi_p8 a b: ordinalp a -> ordinalp b -> (maximal_critical a (Spsi a b)).
proof: Proof. move => oa ob. have[c oc h]: exists2 c, ordinalp c & Spsi a b = Sphi a c. by rewrite /Spsi; Ytac h; [ exists (osucc b); fprops | exists b]. apply/ (maximal_criticalP oa (OS_Spsi oa ob)); rewrite h. exists c; [ exact: (Spsi_p1 oa ob oc h) | reflexivity]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)