proposition: Lemma osum_Meqltr 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 olt. case: (oleT_el ob oa) => // oba. case:(oltNge olt); exact: (osum_Mlele (oleR oc) oba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)