proposition: Lemma aut_dvdn : #[aut_of] %| #[a].
proof: Proof. rewrite order_Zp1 /aut_of; case: pickP => [s | _]; last by rewrite order1. by case/and4P=> _ p_gt1 p_s _; rewrite Zp_cast. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal)