proposition: Lemma last_changeE2 k (s : seq A) : last k s != k -> forall x, x \notin s -> last x s != x.
proof: Proof. by move/last_change/last_notin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)