proposition: Lemma subnormalEsupport G H : H <|<| G -> H :=: G \/ <<class_support H G>> \proper G.
proof: Proof. case/andP=> sHG; set K := <<_>> => /eqP <-. have: K \subset G by rewrite gen_subG class_support_subG. rewrite subEproper; case/predU1P=> [defK|]; [left | by right]. by elim: #|G| => //= _ ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)