proposition: Lemma fsinjectivebP f : reflect (exists2 S : {fset K}, (finsupp f `<=` S) & {in S &, injective f} /\ forall a : S, f (val a) \in S) (fsinjectiveb f).
proof: Proof. by apply/(iffP (fsinjectiveP _)) => /(fsinjP 0 2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)