proposition: Lemma oprod_Meqler a b c: ordinalp a -> ordinalp b -> \0o <o 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 (oprod_Meqlt h1 oc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)