proposition: Lemma mulsgP A B x : reflect (imset2_spec mulg (mem A) (fun _ => mem B) x) (x \in A * B).
proof: Proof. exact: imset2P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)