proposition: Lemma lone_subgroup_char G H : H \subset G -> (forall K, K \subset G -> K \isog H -> K \subset H) -> H \char G.
proof: Proof. move=> sHG Huniq; apply/charP; split=> // f injf Gf; apply/eqP. have{} injf: {in H &, injective f}. by move/injmP: injf; apply: sub_in2; apply/subsetP. have fH: f @* H = f @: H by rewrite /morphim (setIidPr sHG). rewrite eqEcard {2}fH card_in_imset ?{}Huniq //=. by rewrite -{3}Gf morphimS. rewrite isog_sym; apply/isogP. exists [morphism of restrm sHG f] => //=; first exact/injmP. by rewrite morphimEdom fH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)