proposition: Lemma logn_quotient_cent_cyclic_pgroup : p.-group C -> cyclic C -> logn p #|G / 'C_G(C)| <= (logn p #|C|).-1.
proof: Proof. move=> pC cycC; have [-> | ntC] := eqsVneq C 1. by rewrite cent1T setIT trivg_quotient cards1 logn1. have [p_pr _ [e oC]] := pgroup_pdiv pC ntC. rewrite -ker_conj_aut (card_isog (first_isog_loc _ _)) //. apply: leq_trans (dvdn_leq_log _ _ (cardSg (Aut_conj_aut _ _))) _ => //. rewrite card_Aut_cyclic // oC totient_pfactor //= logn_Gauss ?pfactorK //. by rewrite prime_coprime // gtnNdvd // -(subnKC (prime_gt1 p_pr)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)