proposition: Lemma index_filter_mono (p : pred A) (ks : seq A) x y : p x -> index x ks <= index y ks -> index x (filter p ks) <= index y (filter p ks).
proof: Proof. move=>Px; elim: ks=>[|k ks IH] //=; case P : (p k)=>/=; by case: ifP Px; case: ifP=>// _ /eqP <-; rewrite P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)