proposition: Lemma mroots_sum (R : idomainType) (n : nat) (cs : n.+1.-tuple R) : \sum_(c <- cs) c = - (\prod_(c <- cs) ('X - c%:P))`_n.
proof: Proof. move: (mroots_coeff cs) => /(_ 1); rewrite subSS subn0=> ->. rewrite expr1 mulN1r opprK mesym1E raddf_sum /=. by rewrite big_tuple; apply/eq_bigr=> /= i _; rewrite mevalXU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg