proposition: Lemma cprod_eq0 f: (exists2 i, inc i (domain f) & cardinal (Vg f i) = \0c) -> cprod f = \0c.
proof: Proof. move=> [i idf cVz]; rewrite /cprod. case: (emptyset_dichot (productb f)); first by move => ->; apply: cardinal_set0. by move /setXb_ne2 => h; move: (h i idf)=> /card_nonempty1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)