proposition: Lemma index_last_size_uniq z (s : seq A) : uniq s -> index (last z s) s = (size s).-1.
proof: Proof. elim: s z=>//= x s IH z. case/andP=>Nx U; rewrite eq_sym; case: eqVneq=>H. - by rewrite (last_nochange_nil H Nx). rewrite {}IH //; apply: prednK. by case: {Nx U}s H=>//=; rewrite eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)