proposition: Lemma last_filter_change k p (ks : seq A) : last k (filter p ks) != k -> p (last k (filter p ks)) && (last k (filter p ks) \in ks).
proof: Proof. by move/last_change; rewrite mem_filter. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)