proposition: Lemma fsinjP {f} : [<-> injective f; let S := finsupp f in {in S &, injective f} /\ forall a : S, f (val a) \in S; exists2 S : {fset K}, (finsupp f `<=` S) & {in S &, injective f} /\ forall a : S, f (val a) \in S].
proof: Proof. do ?[apply: AllIffConj] => [f_inj|[f_inj f_st]|[S fS [f_inj f_st]] a b]. - split=> [a b ? ?|a]; first exact: f_inj. rewrite mem_finsupp (inj_eq f_inj) -mem_finsupp; apply/valP. - by exists (finsupp f)=> //; apply: fsubset_refl. have Nfinsupp := contra (fsubsetP fS _). wlog /andP [aS bNS] : a b / (a \in S) && (b \notin S) => [hwlog|]; last first. rewrite (fsfun_dflt (Nfinsupp _ bNS)) => fb_eq_a. by move: bNS; rewrite -fb_eq_a (f_st.[aS]). have [[aS|aNS] [bS|bNS]] := (boolP (a \in S), boolP (b \in S)); first 3 last. - by rewrite !fsfun_dflt // ?Nfinsupp. - exact: f_inj. - by apply: hwlog; rewrite aS. by move=> fab; symmetry; apply: hwlog; rewrite // bS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)