proposition: Lemma Spsi_p9 a b: ordinalp a -> ordinalp b -> (maximal_critical a b <-> (exists2 c, ordinalp c & b = Spsi a c)).
proof: Proof. move => oa ob; split; last by move => [c oc ->]; apply:Spsi_p8. move => /(maximal_criticalP oa ob) [c ca eq]. have oc:= proj31_1 ca. case: (p_or_not_p (Spsi_aux a c)); last first. by move => h; exists c => //; rewrite /Spsi; Ytac0. move => [n [d [oi od pd pe]]]. have on: ordinalp n:= proj31_1 oi. case: (ordinal_limA on) => nz. + have bc: c = d by move: pd; rewrite nz (osum0r od). by move: pe (nesym (proj2 ca)); rewrite - bc - eq. + move: (predo_K nz); set m := opred n => sm. have om: ordinalp m by apply:OS_sup => t /(Os_ordinal on). have ocm:= OS_sum2 od om. have spa: (Spsi_aux a (d +o m)). exists m, d; split => //; move: (oltS om); rewrite sm =>h. exact (olt_ltT h oi). exists (d +o m) => //;rewrite /Spsi; Ytac0. by rewrite osum2_succ // sm - pd. case:(oltNge oi (limit_ge_omega nz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)