proposition: Lemma indexlast_subseq (s1 s2 : seq A) a b : subseq s1 s2 -> uniq s2 -> a \in s1 -> b \in s1 -> indexlast a s1 < indexlast b s1 <-> indexlast a s2 < indexlast b s2.
proof: Proof. by case/subseqP=>m _ ->; apply: indexlast_mask. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)