proposition: Lemma normal_subnormal H G : H <| G -> H <|<| G.
proof: Proof. by move=> nsHG; apply/subnormalP; exists [:: G]; rewrite //= nsHG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)