proposition: Lemma normsP A B : reflect {in A, normalised B} (A \subset 'N(B)).
proof: Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. by apply/normP; apply: nBA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)