proposition: Lemma index_filter_ltL (p : pred A) (ks : seq A) (t1 t2 : A) : (t1 \notin ks) || p t1 -> (index t1 ks < index t2 ks) -> (index t1 (filter p ks) < index t2 (filter p ks)).
proof: Proof. elim: ks t1 t2=>[|k ks IH] t1 t2 //=; rewrite inE negb_or (eq_sym t1). case: eqP=>[->{k} /= Pt1|/eqP Nkt1 /= H]. - by rewrite Pt1 /= eqxx; case: eqP. case: eqP=>// /eqP Nkt2; case: ifP=>H1 /=. - by rewrite (negbTE Nkt1) (negbTE Nkt2) !ltnS; apply: IH H. by rewrite ltnS; apply: IH H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)