proposition: Lemma size_weighted_sum_leq (A :eqType) (r : seq A) m (f : A -> R) (g : A -> {poly R}) : (forall i, i \in r -> (size (g i) <= m)%N) -> (size (\sum_(i <- r) f i *: g i)%R <= m)%N.
proof: Proof. elim: r => [_ | n r IH cg]; first by rewrite big_nil polyseq0. rewrite big_cons (leq_trans (size_add _ _)) // geq_max. have sn : (size (f n *: g n) <= m)%N. case fn : (f n == 0); first by rewrite (eqP fn) scale0r size_poly0. rewrite size_scale; last by rewrite fn. by apply: (cg n); rewrite in_cons eqxx. by rewrite sn /=; apply: IH => i ir; apply: cg; rewrite in_cons ir orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc