proposition: Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)).
proof: Proof. rewrite gen_subG; apply/subsetP/subsetP=> [sRH x Gx | nGH xy]. rewrite inE; apply/subsetP=> _ /imsetP[y Ky ->]. by rewrite conjg_Rmul groupMr // sRH // imset2_f ?groupV. case/imset2P=> x y Gx Hy ->{xy}. by rewrite commgEr groupMr // memJ_norm (groupV, nGH). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)