proposition: Lemma NS_in_product a b: cardinalp a -> b <> \0c -> natp (a *c b) -> natp a.
proof: Proof. move=> ca nzb. have on: (\1c <=c (cardinal b)). apply: cge1; [fprops | by apply: card_nonempty0]. rewrite -(cprod2cr a b) -(cdiff_pr on) cprodDr (cprod1r ca). apply: (NS_in_suml ca). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)