proposition: Lemma osum_Meqler a b c: ordinalp a -> ordinalp b -> ordinalp c -> c +o a <=o c +o b -> a <=o b.
proof: Proof. move => oa ob oc h. case: (oleT_el oa ob) => // h1; case: (oleNgt h (osum_Meqlt h1 oc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)