proposition: Lemma poly_ext (R : ringType) (n : nat) (E1 E2 : nat -> R) : (forall i : nat, (i < n)%N -> E1 i = E2 i) -> \poly_(i < n) E1 i = \poly_(i < n) E2 i.
proof: Proof. by move=> E; rewrite !poly_def; apply: eq_bigr => i _; rewrite E. 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