proposition: Lemma osum_Mlteqr a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a +o c) <o (b +o c) -> a <o b.
proof: Proof. move => oa ob oc olt. case: (oleT_el ob oa) => // oba. case: (oltNge olt); exact: (osum_Mlele oba (oleR oc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)