proposition: Lemma maxnormal_minnormal G L M : G \subset 'N(M) -> L \subset 'N(G) -> maxnormal M G L -> minnormal (G / M) (L / M).
proof: Proof. move=> nMG nGL /maxgroupP[/andP[/andP[sMG ltMG] nML] maxM]; apply/mingroupP. rewrite -subG1 quotient_sub1 ?ltMG ?quotient_norms //. split=> // Hb /andP[ntHb nHbL]; have nsMG: M <| G by apply/andP. case/inv_quotientS=> // H defHb sMH sHG; rewrite defHb; congr (_ / M). apply/eqP; rewrite eqEproper sHG /=; apply: contra ntHb => ltHG. have nsMH: M <| H := normalS sMH sHG nsMG. rewrite defHb quotientS1 // (maxM H) // ltHG /= -(quotientGK nsMH) -defHb. exact: norm_quotient_pre. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)