proposition: Lemma mem_drop_indexlast x s : x \notin drop (indexlast x s).+1 s.
proof: Proof. elim: s=>//=h s; rewrite indexlast_cons. case: eqP=>//= _ H. by case: ifP=>//=; rewrite drop0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)