proposition: Lemma primJ n (w : F) : n.-primitive_root w -> n.-primitive_root (w^-1).
proof: Proof. move/andP=> [nP /forallP H]; apply/andP; split => //. apply/forallP => i; apply/eqP; rewrite -(eqP (H i)). by apply: unity_rootJ. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn