proposition: Lemma recip_sum n (g : nat -> {poly R}) : (forall i : 'I_n, (size (g i) <= deg.+1)%N) -> recip deg (\sum_(i < n) g i) = \sum_(i < n) recip deg (g i).
proof: Proof. move=> cg; have bigc : forall i : 'I_n, true -> g i = 1 *: g i. by move=> i _; rewrite scale1r. rewrite (eq_bigr _ bigc). rewrite (recip_weighted_sum (fun i => 1%R)); last by []. by apply: eq_bigr=> i _; rewrite scale1r. 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