proposition: Lemma last_nochange k (s : seq A) : last k s = k -> (k \in s) || (s == [::]).
proof: Proof. case: s k=>[|k s] //= k'; rewrite inE; case: eqP=>[->|N L] //. by move: (@last_change k s); rewrite L=>-> //; case: eqP N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)