proposition: Lemma osum_succP a b: ordinalp a -> ordinalp b -> (osuccp (a +o b) <-> ((b = \0c /\ osuccp a) \/ osuccp b)).
proof: Proof. move => oa ob; split. case :(ordinal_limA ob) => ov. - by rewrite ov (osum0r oa) => osa; left. - by right. - move => h; case:(limit_nonsucc' (osum_limit oa ov) h). case; first by move => [-> osa]; rewrite (osum0r oa). move => [c oc ->]; rewrite - (osum2_succ oa oc); exists (a +o c); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)