proposition: Lemma last_filter_neq (p1 p2 : pred A) x (s : seq A) : subpred p1 p2 -> x \notin s -> last x (filter p1 s) != x -> last x (filter p2 s) != x.
proof: Proof. move=>S N /last_filter_change /andP [H1 H2]. apply: (@last_notin (last x [seq x <-s | p1 x])). - by rewrite mem_filter H2 andbT; apply: S. by rewrite mem_filter negb_and N orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)