proposition: Lemma root_exp_XsubC n a x : root (('X - a%:P) ^+ n.+1) x = (x == a).
proof: Proof. by rewrite rootE horner_exp expf_eq0 [_ == 0]root_XsubC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)