proposition: Lemma charP H G : let fixH (f : {morphism G >-> gT}) := 'injm f -> f @* G = G -> f @* H = H in reflect [/\ H \subset G & forall f, fixH f] (H \char G).
proof: Proof. do [apply: (iffP andP) => -[sHG chHG]; split] => // [f injf Gf|]. by apply/morphim_fixP; rewrite // -imset_autE ?(forall_inP chHG) ?Aut_aut. apply/forall_inP=> f Af; rewrite -(autmE Af) -morphimEsub //. by rewrite chHG ?injm_autm ?im_autm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)