proposition: Lemma coef_prod_XsubC (ps : seq R) (n : nat) : (n <= size ps)%N -> (\prod_(p <- ps) ('X - p%:P))`_n = (-1) ^+ (size ps - n)%N * \sum_(I in {set 'I_(size ps)} | #|I| == (size ps - n)%N) \prod_(i in I) ps`_i.
proof: Proof. move=> nle. under eq_bigr => i _ do rewrite addrC -raddfN/=. rewrite -{1}(in_tupleE ps) -(map_tnth_enum (_ ps)) big_map. rewrite enumT bigA_distr /= coef_sum. transitivity (\sum_(I in {set 'I_(size ps)}) if #|I| == (size ps - n)%N then \prod_(i < size ps | i \in I) - ps`_i else 0). apply eq_bigr => I _. rewrite big_if/= big_const iter_mulr_1 -rmorph_prod/= coefCM coefXn. under eq_bigr => i _ do rewrite (tnth_nth 0)/=. rewrite -[#|I| == _](eqn_add2r n) subnK//. rewrite -[X in (_ + _)%N == X]card_ord -(cardC I) eqn_add2l. by case: ifP; rewrite ?mulr1 ?mulr0. by rewrite -big_mkcond mulr_sumr/=; apply: eq_bigr => I /eqP <-; rewrite prodrN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)