proposition: Lemma imset_mulgm (A B : {set gT}) : mulgm @: setX A B = A * B.
proof: Proof. by rewrite -curry_imset2X. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)