proposition: Lemma indexlast_inj x y s : x \in s -> indexlast x s = indexlast y s -> x = y.
proof: Proof. elim: s=>[|k s IH] //=; rewrite inE eq_sym !indexlast_cons. case: eqP=>[->{k} _|_ /= S] /=. - case: eqP=>//= _. by case: ifP=>// /negbT; rewrite negbK=>H; case; apply: IH. by case: ifP=>// _ []; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)