proposition: Lemma cent_sub A : 'C(A) \subset 'N(A).
proof: Proof. apply/subsetP=> x /centP cAx; rewrite inE. by apply/subsetP=> _ /imsetP[y Ay ->]; rewrite /conjg -cAx ?mulKg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)