proposition: Lemma minnormal_maxnormal G L M : M <| G -> L \subset 'N(M) -> minnormal (G / M) (L / M) -> maxnormal M G L.
proof: Proof. case/andP=> sMG nMG nML /mingroupP[/andP[/= ntGM _] minGM]; apply/maxgroupP. split=> [|H /andP[/andP[sHG ltHG] nHL] sMH]. by rewrite /proper sMG nML andbT; apply: contra ntGM => /quotientS1 ->. apply/eqP; rewrite eqEsubset sMH andbT -quotient_sub1 ?(subset_trans sHG) //. rewrite subG1; apply: contraR ltHG => ntHM; rewrite -(quotientSGK nMG) //. by rewrite (minGM (H / M)%G) ?quotientS // ntHM quotient_norms. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)