proposition: Lemma indexlast_cons x y s : indexlast x (y::s) = if (y == x) && (x \notin s) then 0 else (indexlast x s).+1.
proof: Proof. by rewrite /indexlast findlast_cons has_pred1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)