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