proposition: Lemma size_prod_seq (I : eqType) (s : seq I) (F : I -> {poly R}) : (forall i, i \in s -> F i != 0) -> size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N.
proof: Proof. move=> nzF; rewrite big_tnth size_prod; last by move=> i; rewrite nzF ?mem_tnth. by rewrite cardT /= size_enum_ord [in RHS]big_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)