fact: Definition stable_factor A V U := ([~: U, A] \subset V) && (V <| U).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)