proposition: Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x.
proof: Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. move: s_x; rewrite inE; have [-> // | _] := eqVneq; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)