proposition: Lemma Aint_unity_root n x : (n > 0)%N -> n.-unity_root x -> x \in Aint.
proof: Proof. move=> n_gt0 xn1; apply: root_monic_Aint xn1 (monic_Xn_sub_1 _ n_gt0) _. by apply/polyOverP=> i; rewrite coefB coefC -mulrb coefXn /= rpredB ?rpred_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)