proposition: Lemma perm_in_inj : injective (fun x => if x \in A then f x else x).
proof: Proof. move=> x y /=; wlog Ay: x y / y \in A. by move=> IH eqfxy; case: ifP (eqfxy); [symmetry | case: ifP => //]; auto. rewrite Ay; case: ifP => [Ax | nAx def_x]; first exact: injf. by case/negP: nAx; rewrite def_x (subsetP sBf) ?imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)