proposition: Lemma last_change k (s : seq A) : last k s != k -> last k s \in s.
proof: Proof. by move: (mem_last k s); rewrite inE; case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)