proposition: Lemma minnormal_exists G H : H :!=: 1 -> G \subset 'N(H) -> {M : {group gT} | minnormal M G & M \subset H}.
proof: Proof. by move=> ntH nHG; apply: mingroup_exists (H) _; rewrite ntH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)