proposition: Lemma mu_prod_XsubC (x : L) (s : seq L) : mup x (\prod_(x <- s) ('X - x%:P)) = count_mem x s.
proof: Proof. elim: s => [|y s IHs]; rewrite (big_cons, big_nil)/=. by rewrite mupNroot// root1. rewrite mupM ?polyXsubC_eq0// ?monic_neq0 ?monic_prod_XsubC//. by rewrite IHs (@mup_XsubCX 1). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)