proposition: Lemma cprod_increasing6 f j: cardinalp (Vg f j) -> card_nz_fam f -> inc j (domain f) -> (Vg f j) <=c (cprod f).
proof: Proof. move=> cf alnz jd. move: (cprod_increasing1 alnz (set1_sub jd)). by rewrite cprod_trivial4 (card_card cf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)