proposition: Lemma index_geq x s i : x \in drop i s -> i <= indexlast x s.
proof: Proof. by rewrite -has_pred1; apply: find_geq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)