proposition: Lemma index_memN x xs : x \notin xs <-> index x xs = size xs.
proof: Proof. split; first by exact: memNindex. by move=>E; rewrite -index_mem E ltnn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)