proposition: Lemma coef0_prod_XsubC (ps : seq R) : (\prod_(p <- ps) ('X - p%:P))`_0 = (-1) ^+ (size ps) * \prod_(p <- ps) p.
proof: Proof. rewrite coef_prod_XsubC// subn0; congr GRing.mul. transitivity (\sum_(I in [set setT : {set 'I_(size ps)}]) \prod_(i in I) ps`_i). apply: congr_big =>// i/=. apply/idP/set1P => [/eqP cardE | ->]; last by rewrite cardsT card_ord. by apply/eqP; rewrite eqEcard subsetT cardsT card_ord cardE leqnn. rewrite big_set1 -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT. apply: congr_big => // i; first exact: in_setT. by rewrite (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)