proposition: Lemma normD1 A : 'N(A^#) = 'N(A).
proof: Proof. apply/eqP; rewrite eqEsubset normsD1 //. rewrite -{2}(setID A 1) setIC normsU //; apply/normsP=> x _; apply/setP=> y. by rewrite conjIg conjs1g !inE mem_conjg; case: eqP => // ->; rewrite conj1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)