proposition: Lemma norms_cent A B : A \subset 'N(B) -> A \subset 'N('C(B)).
proof: Proof. by move=> nBA; apply: subset_trans nBA (cent_norm B). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)