proposition: Corollary index_sizeE x xs : reflect (index x xs = size xs) (x \notin xs).
proof: Proof. by apply/(equivP idP)/index_memN. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)