proposition: Lemma abelianY A B : abelian (A <*> B) = [&& abelian A, abelian B & B \subset 'C(A)].
proof: Proof. rewrite /abelian join_subG /= centY !subsetI -!andbA; congr (_ && _). by rewrite centsC andbA andbb andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)