proposition: Lemma OhmPredP (x : gT) : reflect (exists2 p, prime p & x ^+ (p ^ n) = 1) (x ^+ (pdiv #[x] ^ n) == 1).
proof: Proof. have [-> | nt_x] := eqVneq x 1. by rewrite expg1n eqxx; left; exists 2; rewrite ?expg1n. apply: (iffP idP) => [/eqP | [p p_pr /eqP x_pn]]. by exists (pdiv #[x]); rewrite ?pdiv_prime ?order_gt1. rewrite (@pdiv_p_elt p) //; rewrite -order_dvdn in x_pn. by rewrite [p_elt _ _](pnat_dvd x_pn) // pnatX pnat_id. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)