proposition: Lemma last_nochange_nil k (s : seq A) : last k s = k -> k \notin s -> s = [::].
proof: Proof. by move/last_nochange; case/orP=>[/negbF ->|/eqP]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)