proposition: Lemma gFid gT (G : {group gT}) : F gT (F gT G) = F gT G.
proof: Proof. apply/eqP; rewrite eqEsubset gFsub. by move/gFhereditary: (gFsub F G); rewrite setIid /=. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)