proposition: Lemma Viete : forall n, \prod_(i < n ) ('X - ('X_i)%:P) = \sum_ (k < n.+1) (-1)^+k *: ('s_(n, k) *: 'X^(n-k)) :> {poly {mpoly int[n]}}.
proof: Proof. elim => [|n ih]. by rewrite !big_ord0 big_ord1 mesym0E expr0 !scale1r. pose F n k : {poly {mpoly int[n]}} := (-1)^+k *: ('s_(n, k) *: 'X^(n-k)). have Fn0 l: F l 0%N = 'X^l. by rewrite /F expr0 mesym0E !scale1r subn0. have Fnn l: F l l = (-1)^+l *: \prod_(i < l) ('X_i)%:P. by rewrite /F mesymnnE subnn expr0 alg_polyC rmorph_prod. rewrite big_ord_recr /=; set p := (\prod_(_ < _) _). have {p}->: p = mpw (\prod_(i < n) ('X - ('X_i)%:P)). rewrite /mpwiden rmorph_prod /=; apply/eq_bigr. move=> /= i _; rewrite raddfB /= map_polyX map_polyC /=. by rewrite mwidenX mnmwiden1. rewrite {}ih (eq_bigr (F n.+1 \o val)) //; apply/esym. rewrite (eq_bigr (F n \o val)) // -!(big_mkord xpredT). rewrite raddf_sum /= mulrBr !mulr_suml. rewrite big_nat_recl 1?[X in X-_]big_nat_recl //. rewrite -!addrA !Fn0; congr (_ + _). by rewrite rmorphXn /= mpwidenX exprSr. rewrite big_nat_recr 1?[X in _-X]big_nat_recr //=. rewrite opprD !addrA; congr (_ + _); last first. rewrite !Fnn !mpwidenZ !rmorphXn /= mwidenN1. rewrite exprS mulN1r scaleNr -scalerAl; congr (- (_ *: _)). rewrite big_ord_recr rmorph_prod /=; congr (_ * _). by apply/eq_bigr=> i _; rewrite mpwidenC mwidenX mnmwiden1. rewrite -sumrB !big_seq; apply/eq_bigr => i /=. rewrite mem_index_iota => /andP [_ lt_in]; rewrite {Fn0 Fnn}/F. rewrite subSS mesymSS !mpwidenZ !rmorphXn /= !mwidenN1 !mpwidenX. rewrite exprS mulN1r !scaleNr mulNr -opprD; congr (-_). rewrite -!scalerAl -scalerDr; congr (_ *: _). rewrite -exprSr -subSn // subSS scalerDl; congr (_ + _). by rewrite -!mul_polyC !mulrA mulrAC polyCM. 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