proposition: Lemma coefPn_prod_XsubC (ps : seq R) : size ps != 0 -> (\prod_(p <- ps) ('X - p%:P))`_((size ps).-1) = - \sum_(p <- ps) p.
proof: Proof. rewrite coef_prod_XsubC ?leq_pred// => ps0. have -> : (size ps - (size ps).-1 = 1)%N. by move: ps0; case: (size ps) => // n _; exact: subSnn. rewrite expr1 mulN1r; congr GRing.opp. set f : 'I_(size ps) -> {set 'I_(size ps)} := fun a => [set a]. transitivity (\sum_(I in imset f (mem setT)) \prod_(i in I) ps`_i). apply: congr_big => // I /=. by apply/cards1P/imsetP => [[a ->] | [a _ ->]]; exists a. rewrite big_imset/=; last first. by move=> i j _ _ ij; apply/set1P; rewrite -/(f j) -ij set11. rewrite -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT. apply: congr_big => // i; first exact: in_setT. by rewrite big_set1 (tnth_nth 0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)