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