proposition: Lemma rmorph_unity_root n z : n.-unity_root z -> n.-unity_root (f z).
proof: Proof. move/rmorph_root; rewrite rootE rmorphB hornerD hornerN. by rewrite /= map_polyXn rmorph1 hornerC hornerXn subr_eq0 unity_rootE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)