proposition: Lemma abelianM G H : abelian (G * H) = [&& abelian G, abelian H & H \subset 'C(G)].
proof: Proof. by rewrite -abelian_gen genM_join abelianY. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)