proposition: Lemma size_prod (I : finType) (P : pred I) (F : I -> {poly R}) : (forall i, P i -> F i != 0) -> size (\prod_(i | P i) F i) = ((\sum_(i | P i) size (F i)).+1 - #|P|)%N.
proof: Proof. move=> nzF; transitivity (\sum_(i | P i) (size (F i)).-1).+1; last first. apply: canRL (addKn _) _; rewrite addnS -sum1_card -big_split /=. by congr _.+1; apply: eq_bigr => i /nzF/polySpred. elim/big_rec2: _ => [|i d p /nzF nzFi IHp]; first by rewrite size_poly1. by rewrite size_mul // -?size_poly_eq0 IHp // addnS polySpred. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)