proposition: Lemma oprod_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: (oprod_Mlele (oleR oc) oba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)