proposition: Lemma sum_supp e x : \sum_(i < n) e ``_ i * x ^+ i = \sum_(i in supp e) e ``_ i * x ^+ i.
proof: Proof. rewrite (bigID (mem (supp e))) /= addrC (eq_bigr (fun=> 0)); last first. move=> ?; rewrite inE /= negbK => /eqP ->; by rewrite mul0r. by rewrite big_const /= iter_addr0 add0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2