proposition: Lemma maxnormalM G H K : maxnormal H G G -> maxnormal K G G -> H :<>: K -> H * K = G.
proof: Proof. move=> maxH maxK /eqP; apply: contraNeq => ltHK_G. have [nsHG nsKG] := (maxnormal_normal maxH, maxnormal_normal maxK). have cHK: commute H K. exact: normC (subset_trans (normal_sub nsHG) (normal_norm nsKG)). wlog suffices: H K {maxH} maxK nsHG nsKG cHK ltHK_G / H \subset K. by move=> IH; rewrite eqEsubset !IH // -cHK. have{maxK} /maxgroupP[_ maxK] := maxK. apply/joing_idPr/maxK; rewrite ?joing_subr //= comm_joingE //. by rewrite properEneq ltHK_G; apply: normalM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)