fact: Definition subnormal A B := (A \subset B) && (iter #|B| (fun N => generated (class_support A N)) B == A).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)