proposition: Lemma osum_Mle0 a b: ordinalp a -> ordinalp b -> a <=o (a +o b).
proof: Proof. move=> oa ob. rewrite - {1} (osum0r oa); apply: osum_Meqle => //; apply:(ole0x ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)