proposition: Lemma quotient_subnormal H G K : G <|<| K -> G / H <|<| K / H.
proof: Proof. exact: morphim_subnormal. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)