fact: Definition hereditary := forall gT (H G : {group gT}), H \subset G -> F G :&: H \subset F H.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)