proposition: Lemma rootZ x a p : a != 0 -> root (a *: p) x = root p x.
proof: Proof. by move=> nz_a; rewrite -mul_polyC rootM rootC (negPf nz_a). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)