proposition: Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) : A \subset 'N(G) -> A \subset 'N(F gT G).
proof: Proof. by move/subset_trans/(_ (gFnorms G)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)