proposition: Lemma normsIs : B \subset 'N(D) -> A :&: B \subset 'N(C :&: D).
proof: Proof. move/normsP=> nDB; apply/normsP=> x; case/setIP=> Ax Bx. by rewrite conjIg (normsP nCA) ?nDB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)