proposition: Lemma index_filter_lt (p : pred A) (ks : seq A) (t1 t2 : A) : (t1 \notin ks) || p t1 -> (t2 \notin ks) || p t2 -> (index t1 (filter p ks) < index t2 (filter p ks)) = (index t1 ks < index t2 ks).
proof: Proof. move=>H1 H2; apply/idP/idP. - by apply: index_filter_ltR. by apply: index_filter_ltL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)