proposition: Lemma last_changeE1 k (s : seq A) : last k s != k -> forall x, last x s = last k s.
proof: Proof. by elim: s k=>[|k s IH] y //=; rewrite eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)