proposition: Lemma mem_take_index x xs : x \notin take (index x xs) xs.
proof: Proof. elim: xs=>//=h xs; case: eqP=>//= /eqP H IH. by rewrite inE negb_or eq_sym H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)