proposition: Lemma gFnormal gT (G : {group gT}) : F gT G <| G.
proof: Proof. exact/char_normal/gFchar. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)