proposition: Lemma group_set_normaliser A : group_set 'N(A).
proof: Proof. apply/group_setP; split=> [|x y Nx Ny]; rewrite inE ?conjsg1 //. by rewrite conjsgM !(normP _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)