proposition: Lemma set_swap (A B : finType) (P : B -> A -> bool) : [set h : {: B * A} | P h.1 h.2 ] = swap @: [set h | P h.2 h.1].
proof: Proof. apply/setP => /= -[b a]; rewrite !inE /=; apply/idP/imsetP => [H|]. - by exists (a, b) => //=; rewrite inE. - by case=> -[a0 b0]; rewrite inE /= => ? [-> ->]. Qed.
imports: mathcomp(all_ssreflect fingroup perm)