proposition: Lemma has_drop p s i : has p s -> has p (drop i s) = (i <= findlast p s).
proof: Proof. rewrite findlastE=>/[dup] E ->; rewrite -has_rev in E. have Hh: 0 < size s - find p (rev s). - by rewrite -size_rev subn_gt0 -has_find. rewrite -size_rev; move/(has_take (size s - i)): (E). rewrite take_rev -subnS size_rev. case/boolP: (i < size s)=>[Hi|]. - rewrite subnA //; last by apply: ltnW. rewrite subnn add0n has_rev=>->. rewrite ltn_subRL addnC -ltn_subRL subnS. by case: (size s - find p (rev s)) Hh. rewrite -ltnNge ltnS => Hi _. rewrite drop_oversize //=; symmetry; apply/negbTE. rewrite -ltnNge subnS prednK //. by apply/leq_trans/Hi; exact: leq_subr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)