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