proposition: Lemma root_exp p n a: comm_poly p a -> (0 < n)%N -> root (p ^+ n) a = root p a.
proof: Proof. by move=> ? n0; rewrite !rootE horner_exp_comm// expf_eq0 n0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)