proposition: Lemma oprod_Mlele a b c d: a <=o b -> c <=o d -> (a *o c) <=o (b *o d).
proof: Proof. move=> le1 le2; apply: (oleT (oprod_Meqle le2 (proj31 le1))). apply:oprod_Mleeq le1 (proj32 le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)