proposition: Lemma maxnormal_charsimple G H L : G <| L -> maxnormal H G L -> charsimple (G / H).
proof: Proof. case/andP=> sGL nGL /maxgroupP[/andP[/andP[sHG not_sGH] nHL] maxH]. have nHG: G \subset 'N(H) := subset_trans sGL nHL. apply/charsimpleP; rewrite -subG1 quotient_sub1 //; split=> // HK ntHK chHK. case/(inv_quotientN _): (char_normal chHK) => [|K defHK sHK]; first exact/andP. case/andP; rewrite subEproper defHK => /predU1P[-> // | ltKG] nKG. have nHK: H <| K by rewrite /normal sHK (subset_trans (proper_sub ltKG)). case/negP: ntHK; rewrite defHK -subG1 quotient_sub1 ?normal_norm //. rewrite (maxH K) // ltKG -(quotientGK nHK) -defHK norm_quotient_pre //. by rewrite (char_norm_trans chHK) ?quotient_norms. 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)