proposition: Lemma dvdn_prime_cyclic G p : prime p -> #|G| %| p -> cyclic G.
proof: Proof. move=> p_pr pG; case: (eqsVneq G 1) => [-> | ntG]; first exact: cyclic1. by rewrite prime_cyclic // (prime_nt_dvdP p_pr _ pG) -?trivg_card1. 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)