proposition: Lemma normC A B : A \subset 'N(B) -> commute A B.
proof: Proof. move/subsetP=> nBA; apply/setP=> u. apply/mulsgP/mulsgP=> [[x y Ax By] | [y x By Ax]] -> {u}. by exists (y ^ x^-1) x; rewrite -?conjgCV // memJ_norm // groupV nBA. by exists x (y ^ x); rewrite -?conjgC // memJ_norm // nBA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)