proposition: Lemma cent_norm A : 'N(A) \subset 'N('C(A)).
proof: Proof. by apply/normsP=> x nCx; rewrite -centJ (normP nCx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)