proposition: Lemma comm_joingE G H : commute G H -> G <*> H = G * H.
proof: Proof. by move/comm_group_setP=> gGH; rewrite -genM_join; apply: (genGid (group gGH)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)