proposition: Lemma gFnorms gT (G : {group gT}) : 'N(G) \subset 'N(F gT G).
proof: Proof. exact/char_norms/gFchar. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)