proposition: Lemma recip_weighted_sum n (f : nat -> R) (g : nat -> {poly R}) : (forall i : 'I_n, (size (g i) <= deg.+1)%N) -> recip deg (\sum_(i < n) f i *: g i) = \sum_(i < n) f i *: (recip deg (g i)).
proof: Proof. elim: n => [ | n IH cg]; first by rewrite !big_ord0 recip0. rewrite !big_ord_recr /=. rewrite recipD; first last. case fn0 : (f n == 0); first by rewrite (eqP fn0) scale0r size_poly0. by rewrite size_scale ?fn0 // (cg ord_max). apply: size_weighted_sum_leq. by move=> [i ci] _; apply: (cg (Ordinal _)); rewrite ltnS ltnW. rewrite IH ?recipZ //; first by apply: (cg ord_max). by move=> [i ci]; apply: (cg (Ordinal _)); rewrite ltnS ltnW. 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