proposition: Theorem cprod_nzP f: card_nz_fam f <-> (cprod f <> \0c).
proof: Proof. split => h. have alne: (forall i, inc i (domain f) -> nonempty (Vg f i)). move=> i /h vz;case: (emptyset_dichot (Vg f i))=> // p. move: (setXb_ne alne); apply: card_nonempty1. move=> i idf /=; dneg vz; apply: cprod_eq0=>//; ex_tac. by rewrite vz; apply: cardinal_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)