proposition: Lemma indexlast1 x y : indexlast x [::y] = (x != y).
proof: Proof. by rewrite /indexlast findlast1 /= eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)