proposition: Lemma nt_gen_prime G x : prime #|G| -> x \in G^# -> G :=: <[x]>.
proof: Proof. move=> Gpr /setD1P[]; rewrite -cycle_subG -cycle_eq1 => ntX sXG. apply/eqP; rewrite eqEsubset sXG andbT. by apply: contraR ntX => /(prime_TIg Gpr); rewrite (setIidPr sXG) => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)