proposition: Lemma subnormal_trans K H G : H <|<| K -> K <|<| G -> H <|<| G.
proof: Proof. case/subnormalP=> [s1 Hs1 <-] /subnormalP[s2 Hs12 <-]. by apply/subnormalP; exists (s1 ++ s2); rewrite ?last_cat // cat_path Hs1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)