proposition: Lemma ofinite_plus_infinite x y: finite_o x -> ordinalp y -> infinite_o y -> x +o y = y.
proof: Proof. move: OS_omega=> oo ha hb /(omega_P1 hb) hc. move /omega_P2: (ha) => /(oltP oo) /osum_int_omega hd. by apply: (ord_negl_sum' (proj1 ha) hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)