proposition: Lemma Spsi_p5 a b: ordinalp a -> ordinalp b -> (a <o Spsi a b <-> ~ (strong_critical (Spsi a b))).
proof: Proof. move => oa ob; set c := Spsi a b. have oc: ordinalp c by apply: OS_Spsi. case (equal_or_not (Sphi c \0o) c) => eq1. split; last by move => h; move/(strong_criticalP oc): eq1. move:(Spsi_p0 oc); rewrite eq1; move/(Spsi_p4 oc oa OS0 ob). by move => [-> _] [_]. split; first by move => _ h; move/(strong_criticalP oc): eq1. move => _. have: c <o Sphi c \0o. split; [ exact:(osi_gex (proj1 (Sphi_p5)) oc) | by apply:nesym]. rewrite{1}/c /Spsi; set d := Yo _ _ _. have od: ordinalp d. rewrite /d; Ytac h; fprops. move/(Sphi_p7 od OS0 oa oc) => [qa qb qc]. case: (oleT_ell oa oc) => h. - by move: (qb h) => /olt0. - exact h. - by move: (qc h) => /olt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)