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