proposition: Lemma unity_rootE n z : n.-unity_root z = (z ^+ n == 1).
proof: Proof. by rewrite /root_of_unity rootE hornerD hornerN hornerXn hornerC subr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)