proposition: Lemma cprod_M1le a b: cardinalp a -> b <> \0c -> a <=c (a *c b).
proof: Proof. move=> ca nbz. rewrite -{1}(cprod1r ca) - (cprod2cr a b). apply: cprod_Mlele; fprops; apply: cge1; fprops. by apply: card_nonempty0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)