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