proposition: Lemma strong_criticalP x: ordinalp x -> (strong_critical x <-> Sphi x \0o = x).
proof: Proof. move => ox;split; last by move => h; exists \0o; fprops. move => [y oy yb]; move: (Sphi_p9 ox); rewrite {1} yb => h. case: (ozero_dichot oy); first by move => <-. by move / (proj1 (Sphi_p1 ox)) => /(oleNgt h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)