proposition: Lemma nontrivial_gacent_pgroup G M : p.-group G -> p.-group M -> {acts G, on group M | to} -> M :!=: 1 -> 'C_(M | to)(G) :!=: 1.
proof: Proof. move=> pG pM [nMG sMR] ntM; have [p_pr p_dv_M _] := pgroup_pdiv pM ntM. rewrite -cardG_gt1 (leq_trans (prime_gt1 p_pr)) 1?dvdn_leq ?cardG_gt0 //= /dvdn. by rewrite gacentE ?(acts_dom nMG) // setIA (setIidPl sMR) -pgroup_fix_mod. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)