proposition: Lemma osum_limit_alt x y: ordinalp x -> limit_ordinal y -> limit_ordinal (x +o y).
proof: Proof. move=> ox ly. move:(proj31 ly) => oy. case: (ozero_dichot ox) => xz; first by rewrite xz osum0l //. move /limit_ordinal_P:ly => [ ynz yl]. move: (@osum_Meqlt \0o y x ynz ox); rewrite (osum0r ox) => lt0. apply /limit_ordinal_P; split; first exact: (olt_ltT xz lt0). move => z lt1. have y1: \1o <o y by rewrite - osucc_zero; apply: yl. have oz:= proj31_1 lt1. rewrite - (osucc_pr oz). case: (oleT_ee oz ox) => zx. exact (ole_ltT (osum_Mleeq zx OS1) (osum_Meqlt y1 ox)). move: (odiff_pr zx) => [pd pe]. rewrite pe in lt1. move: (yl _ (osum_Meqltr pd oy ox lt1)). rewrite - (osucc_pr pd) => pg. by move: (osum_Meqlt pg ox); rewrite (osumA ox pd OS1) -pe. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)