proposition: Lemma last_filter_last (p : pred A) x (s : seq A) y : uniq (x :: s) -> p y -> y \in s -> index y (x :: s) <= index (last x (filter p s)) (x :: s).
proof: Proof. move=>/= /andP [Sx U] H Sy /=; case: (x =P y)=>//= _. have Hy : y \in [seq x <- s | p x] by rewrite mem_filter H Sy. rewrite eq_sym; case: (last x _ =P x); last first. - by move=>_; apply: last_filter_last_helper=>//=; rewrite Sx U. move/last_nochange; rewrite mem_filter (negbTE Sx) andbF /=. by move/eqP=>E; rewrite E in Hy. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)