proposition: Lemma last_notin_nilp k (s : seq A) : ~~ nilp s -> k \notin s -> last k s != k.
proof: Proof. move=>N; apply: (last_notin (x := head k s)). by case: s N=>//= x s _; rewrite inE eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)