proposition: Lemma imset_preimset (I J : finType) (h : I -> J) (B : {set J}) : B \subset h @: I -> h @: (h @^-1: B) = B.
proof: Proof. move/subsetP=> B_covered. apply/setP/subset_eqP/andP. split; apply/subsetP => x; first by case/imsetP => i; rewrite inE => H ->. move=> xB; case/(B_covered x)/imsetP: (xB) => y yI xhy. by apply/imsetP; exists y => //; rewrite inE -xhy. Qed.
imports: mathcomp(all_ssreflect fingroup perm)