proposition: Lemma indexlast_count x s : count_mem x s <= 1 <-> index x s = indexlast x s.
proof: Proof. elim: s=>//= h t IH; rewrite indexlast_cons. case: eqP=>/= ?; last first. - by rewrite add0n IH; split=>[->|[]]. rewrite add1n ltnS leqn0; split. - by move/eqP/count_memPn=>->. by case: ifP=>//= /count_memPn->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)