proposition: Lemma size_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) : size (\sum_(i <- r | P i) F i) <= \max_(i <- r | P i) size (F i).
proof: Proof. elim/big_rec2: _ => [|i p q _ IHp]; first by rewrite size_poly0. by rewrite -(maxn_idPr IHp) maxnA leq_max size_add. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)