proposition: Lemma root_prod_XsubC rs x : root (\prod_(a <- rs) ('X - a%:P)) x = (x \in rs).
proof: Proof. elim: rs => [|a rs IHrs]; first by rewrite rootE big_nil hornerC oner_eq0. by rewrite big_cons rootM IHrs root_XsubC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)