proposition: Lemma find_geq p s i : has p (drop i s) -> i <= findlast p s.
proof: Proof. case/boolP: (has p s)=>Hp; first by rewrite (has_drop _ Hp). suff: ~~ has p (drop i s) by move/negbTE=>->. move: Hp; apply: contra; rewrite -{2}(cat_take_drop i s) has_cat=>->. by rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)