proposition: Lemma last_in x k (s : seq A) : x \in s -> last k s \in s.
proof: Proof. elim: s k=>[|k s IH] k' //=; rewrite !inE. case/orP=>[/eqP <-|/IH ->]; first by apply: mem_last. by rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)