proposition: Corollary index_lt_last x s : 1 < count_mem x s -> index x s < indexlast x s.
proof: Proof. move=>H; move: (index_leq_last x s); rewrite leq_eqVlt. by case: eqP=>//= /indexlast_count; case: leqP H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)