proposition: Lemma commg_subI A B G H : A \subset 'N_G(H) -> B \subset 'N_H(G) -> [~: A, B] \subset G :&: H.
proof: Proof. rewrite !subsetI -(gen_subG _ 'N(G)) -(gen_subG _ 'N(H)). rewrite -commg_subr -commg_subl; case/andP=> sAG sRH; case/andP=> sBH sRG. by rewrite (subset_trans _ sRG) ?(subset_trans _ sRH) ?commgSS ?subset_gen. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)