proposition: Lemma abelem_charsimple p G : p.-abelem G -> G :!=: 1 -> charsimple G.
proof: Proof. move=> abelG ntG; apply/charsimpleP; split=> // K ntK /charP[sKG chK]. case/eqVproper: sKG => // /properP[sKG [x Gx notKx]]. have ox := abelem_order_p abelG Gx (group1_contra notKx). have [A [sAG oA defA]] := p_abelem_split1 abelG Gx. case/trivgPn: ntK => y Ky nty; have Gy := subsetP sKG y Ky. have{nty} oy := abelem_order_p abelG Gy nty. have [B [sBG oB defB]] := p_abelem_split1 abelG Gy. have: isog A B; last case/isogP=> fAB injAB defAB. rewrite (isog_abelem_card _ (abelemS sAG abelG)) (abelemS sBG) //=. by rewrite oA oB ox oy. have: isog <[x]> <[y]>; last case/isogP=> fxy injxy /= defxy. by rewrite isog_cyclic_card ?cycle_cyclic // [#|_|]oy -ox eqxx. have cfxA: fAB @* A \subset 'C(fxy @* <[x]>). by rewrite defAB defxy; case/dprodP: defB. have injf: 'injm (dprodm defA cfxA). by rewrite injm_dprodm injAB injxy defAB defxy; apply/eqP; case/dprodP: defB. case/negP: notKx; rewrite -cycle_subG -(injmSK injf) ?cycle_subG //=. rewrite morphim_dprodml // defxy cycle_subG /= chK //. have [_ {4}<- _ _] := dprodP defB; have [_ {3}<- _ _] := dprodP defA. by rewrite morphim_dprodm // defAB defxy. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)