proposition: Lemma centM G H : 'C(G * H) = 'C(G) :&: 'C(H).
proof: Proof. by rewrite -cent_gen genM_join centY. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)