proposition: Lemma ord_cofinal_p3 a: limit_ordinal a -> (\osup a = \osup (osucc a) /\ ~(ord_cofinal a (osucc a))).
proof: Proof. move => la; move: (la) => [oa _ _]. rewrite - [union a](limit_nonsucc la). split; first by rewrite [union _] succo_K. move => [h1 h2]. have: inc a (osucc a) by rewrite /osucc; fprops. by move/h2 => [y /(oltP oa) ya] /(oltNge ya). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)