proposition: Lemma eq_last (s : seq A) x y : x \in s -> last y s = last x s.
proof: Proof. by elim: s x y=>[|w s IH]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)