proposition: Lemma poly_extend (m n : nat) (E : nat -> R) : (m <= n)%N -> (forall i : nat, (m <= i < n)%N -> E i = 0) -> \poly_(i < m) E i = \poly_(i < n) E i.
proof: Proof. move=> c e; rewrite !poly_def. rewrite (big_ord_widen n (fun i => E i *: 'X^i) c) big_mkcond /=. apply: eq_bigr; move=> [i ci] _ /=; case h: (i < m)%N => //. rewrite e; first by rewrite scale0r. by rewrite ci andbT leqNgt h. 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