proposition: Lemma gFchar gT (G : {group gT}) : F gT G \char G.
proof: Proof. apply/andP; split => //; first by apply: gFsub. apply/forall_inP=> f Af; rewrite -{2}(im_autm Af) -(autmE Af). by rewrite -morphimEsub ?gFsub ?gFiso_cont ?injm_autm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)