proposition: Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| -> cyclic (Aut G).
proof: Proof. move=> pr_G; case/cyclicP: (prime_cyclic pr_G) (pr_G) => x ->. exact: Aut_prime_cycle_cyclic. 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)