proposition: Lemma mulg_normal_maximal G M H : M <| G -> maximal M G -> H \subset G -> ~~ (H \subset M) -> (M * H = G)%g.
proof: Proof. case/andP=> sMG nMG /maxgroupP[_ maxM] sHG not_sHM. apply/eqP; rewrite eqEproper mul_subG // -norm_joinEr ?(subset_trans sHG) //. by apply: contra not_sHM => /maxM <-; rewrite ?joing_subl ?joing_subr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)