proposition: Lemma indexlast_cat x s1 s2 : indexlast x (s1 ++ s2) = if (x \in s1) && (x \notin s2) then indexlast x s1 else size s1 + indexlast x s2.
proof: Proof. by rewrite /indexlast findlast_cat !has_pred1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)