proposition: Lemma quotient_simple gT (G H : {group gT}) : H <| G -> simple (G / H) = maxnormal H G G.
proof: Proof. move=> nsHG; have nGH := normal_norm nsHG. by apply/idP/idP; [apply: minnormal_maxnormal | apply: maxnormal_minnormal]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)