proposition: Lemma p'group_quotient_cent_prime : prime p -> #|C| %| p -> p^'.-group (G / 'C_G(C)).
proof: Proof. move=> p_pr pC; have pgC: p.-group C := pnat_dvd pC (pnat_id p_pr). have [_ dv_p] := primeP p_pr; case/pred2P: {dv_p pC}(dv_p _ pC) => [|pC]. by move/card1_trivg->; rewrite cent1T setIT trivg_quotient pgroup1. have le_oGC := logn_quotient_cent_cyclic_pgroup pgC. rewrite /pgroup -partn_eq1 ?cardG_gt0 // -dvdn1 p_part pfactor_dvdn // logn1. by rewrite (leq_trans (le_oGC _)) ?prime_cyclic // pC ?(pfactorK 1). 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)