proposition: Lemma osum_limit x y: ordinalp x -> limit_ordinal y -> limit_ordinal (x +o y).
proof: Proof. by move=> ox ly; apply:normal_ofs_limit=> //; apply: osum_normal. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)