proposition: Lemma generalizedNewton (l : seq R) (n m : nat) (s := size l) : (n <= m)%N -> (\sum_(x <- l) x) ^+ n = \sum_(t : s.-tuple 'I_m.+1 | (\sum_(i <- t) i)%N == n) ('C[tmap_val t])%:R * monomial l (tmap_val t).
proof: Proof. rewrite {}/s; elim/last_ind: l n m => [|l a ihl] n m /=. - rewrite big_tuple0 big_nil big_tuple big_ord0 /= monom_nill mulr1 /= expr0n. by rewrite multi_nil; case: n. - move=> leqnm; rewrite size_rcons big_rcons /= exprDn. set s := size l. pose tlast s (t : s.-tuple 'I_m.+1) := last ord0 t. have -> P F : \sum_(t : s.+1.-tuple 'I_m.+1 | P t) F t = \sum_(j < m.+1) \sum_(t | P t && (tlast _ t == j)) F t. exact: partition_big. pose F (i : nat) := (\sum_(j <- l) j) ^+ (n - i) * a ^+ i *+ 'C(n, i). have -> : \sum_(i < n.+1) F i = \sum_(i < m.+1 | (i < n.+1)%N) F i. by apply: big_ord_widen; rewrite ltnS. rewrite big_mkcond /=; apply: eq_bigr => i _; case: ltnP=> hni; last first. rewrite /tlast big_pred0 // => [[]]; case/lastP => // t u stu /=. rewrite last_rcons big_rcons /=. by apply: contraTF hni; case/andP=> /eqP<- /eqP<-; rewrite -leqNgt leq_addl. rewrite {}/F. have /ihl -> : (n - i <= m)%N. by apply: (leq_trans (leq_subr _ _)); apply: (leq_trans leqnm). rewrite mulr_suml -sumrMnl. pose tsum a (t : a.-tuple 'I_m.+1) b := ((\sum_(j <- t) j) == b)%N. have -> F : \sum_(t : s.+1.-tuple 'I_m.+1 | tsum _ t n && (tlast _ t == i)) F t = \sum_(t : s.-tuple 'I_m.+1 | tsum _ t (n - i)%N) F [tuple of (rcons t i)]. pose indx (t : s.-tuple 'I_m.+1) := [tuple of rcons t i]. pose indxV (t : s.+1.-tuple 'I_m.+1) := [tuple of rev (behead (rev t))]. rewrite [LHS](reindex indx) /= /tlast /tsum. apply: eq_bigl => t; rewrite last_rcons eqxx andbT big_rcons /=. apply/eqP/eqP=> [|->]; first exact: (canRL (addnK i)). by rewrite subnK. exists indxV => t ht; rewrite /indx /indxV /=; apply: val_inj => /=. by rewrite rev_rcons revK. move: ht; rewrite inE; case/andP=> _; case: t; case/lastP => //= ? j _. by rewrite last_rcons => /eqP->; rewrite rev_rcons /= revK. symmetry; apply: congr_big => //= u /eqP es /=. rewrite tmap_val_rcons multi_rcons natrM mulrAC monom_rcons; last first. by rewrite size_map size_tuple. by rewrite /tmap_val big_map es exprnP mulr_natr -mulrA subnK. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp