proposition: Lemma last_filter_eq (p1 p2 : pred A) x (s : seq A) : subpred p1 p2 -> x \notin s -> last x (filter p2 s) = x -> last x (filter p1 s) = x.
proof: Proof. move=>S N /eqP E; apply/eqP. by apply: contraTT E; apply: last_filter_neq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)