proposition: Lemma comm_group_setP G H : reflect (commute G H) (group_set (G * H)).
proof: Proof. rewrite /group_set (subsetP (mulG_subl _ _)) ?group1 // andbC. have <-: #|G * H| <= #|H * G| by rewrite -invMG card_invg. by rewrite -mulgA mulGS mulgA mulSG -eqEcard eq_sym; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)