proposition: Lemma mroots_coeff (R : idomainType) n (cs : n.-tuple R) (k : 'I_n.+1) : (\prod_(c <- cs) ('X - c%:P))`_(n - k) = (-1)^+k * 's_(n, k).@[tnth cs].
proof: Proof. pose P := (\prod_(i < n) ('X - ('X_i)%:P) : {poly {mpoly int[n]}}). pose f := mmap intr (tnth cs): {mpoly int[n]} -> R. pose F := fun i => 'X - (tnth cs i)%:P. move: (Viete n) => /(congr1 (map_poly f)). rewrite rmorph_prod /= (eq_bigr F); last first. move=> i _; rewrite raddfB /= map_polyX map_polyC /=. by rewrite mmapX mmap1U. rewrite big_tuple => ->; rewrite raddf_sum coef_sum /=. rewrite (bigD1 k) //= big1 ?addr0; last first. case=> i /= lt_iSk; rewrite eqE /= => ne_ik. rewrite !map_polyZ /= map_polyXn !coefZ coefXn. rewrite -(eqn_add2r i) subnK // addnC. rewrite -(eqn_add2r k) -addnA subnK 1?addnC; last first. by move: (ltn_ord k); rewrite ltnS. by rewrite eqn_add2l (negbTE ne_ik) !mulr0. rewrite !map_polyZ !rmorphXn /= raddfN /= mmapC !coefZ /=. congr (_ * _); rewrite map_polyX coefXn eqxx mulr1. rewrite /mesym; rewrite !raddf_sum /=; apply/eq_bigr. move=> i _; rewrite !rmorph_prod /=; apply/eq_bigr. by move=> j _; rewrite mmapX mmap1U 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