proposition: Lemma size_prod_leq (I : finType) (P : pred I) (F : I -> {poly R}) : size (\prod_(i | P i) F i) <= (\sum_(i | P i) size (F i)).+1 - #|P|.
proof: Proof. rewrite -sum1_card. elim/big_rec3: _ => [|i n m p _ IHp]; first by rewrite size_poly1. have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0. rewrite (leq_trans (size_mul_leq _ _)) // subnS -!subn1 leq_sub2r //. rewrite -addnS -addnBA ?leq_add2l // ltnW // -subn_gt0 (leq_trans _ IHp) //. by rewrite polySpred. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)