proposition: Lemma osum2_lt_omega a b: a <o omega0 -> b <o omega0 -> (a +o b) <o omega0.
proof: Proof. move /olt_omegaP => aN /olt_omegaP bN; apply /olt_omegaP. rewrite osum2_2int; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)