proposition: Corollary indexlast_uniq x s : uniq s -> index x s = indexlast x s.
proof: Proof. move=>H; apply/indexlast_count. by rewrite count_uniq_mem //; apply: leq_b1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)