proposition: Lemma unity_rootJ n (w : F) : n.-unity_root w^-1 = n.-unity_root w.
proof: Proof. apply/unity_rootP/unity_rootP; rewrite exprVn => /eqP. by rewrite invr_eq1 => /eqP. by move=> H; apply/eqP; rewrite invr_eq1. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn