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