proposition: Lemma index_last_mono x k (s : seq A) : uniq s -> x \in s -> index x s <= index (last k s) s.
proof: Proof. elim: s k=>[|k s IH] //= k'; rewrite inE !(eq_sym k). case/andP=>K U; case: (x =P k)=>//= /eqP N X. case: (last k s =P k)=>[/last_nochange|/eqP L]. - by case: eqP X=>[->//|]; rewrite (negbTE K). by apply: leq_trans (IH k U X) _. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)