proposition: Lemma last_filter_last_helper (p : pred A) x (s : seq A) y : uniq (x :: s) -> p y -> y \in s -> index y s <= index (last x (filter p s)) s.
proof: Proof. elim: s x=>[|k s IH] x //=; rewrite !inE !negb_or !(eq_sym _ k). case/andP=>/andP [H1 H2] /andP [H3 H4] Px. case: eqP=> [->|_] //= Ks; case P: (p k)=>/=. - case: eqP=>E; last by apply: IH=>//=; rewrite H3 H4. move: (@last_in y k (filter p s)); rewrite -E !mem_filter. by rewrite Px Ks P (negbTE H3); move/(_ (erefl _)). case: eqP=>E; last by apply: IH=>//=; rewrite H2 H4. by move: H1; rewrite E; move/last_filter_change; rewrite -E P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)