proposition: Lemma fin_img_imset (A B : finType) (f : A -> B) : fin_img f =i f @: A.
proof: Proof. apply/subset_eqP/andP; split; apply/subsetP => b; rewrite mem_undup; case/boolP : [exists a, b == f a]. - by case/existsP => a /eqP ->; rewrite imset_f. - rewrite negb_exists; move/forallP=> bfx. case/mapP => a _ bfa. by move: (bfx a); rewrite bfa => /eqP. - by case/existsP => a /eqP -> _; apply/mapP; exists a; rewrite // mem_enum. - rewrite negb_exists; move/forallP=> bfx. case/imsetP => a _ bfa. by move: (bfx a); rewrite bfa => /eqP. Qed.
imports: mathcomp(all_ssreflect fingroup perm)