proposition: Lemma oprod_M1le a b: \0o <o a -> ordinalp b-> b <=o (a *o b).
proof: Proof. move=> /oge1P oa ob. rewrite - {1} (oprod1l ob); exact: oprod_Mlele oa (oleR ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)