proposition: Lemma eq_poly n E1 E2 : (forall i, i < n -> E1 i = E2 i) -> poly n E1 = poly n E2 :> {poly R}.
proof: Proof. by move=> E; rewrite !poly_def; apply: eq_bigr => i _; rewrite E. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)