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