proposition: Lemma mem_prev p x : (prev p x \in p) = (x \in p).
proof: Proof. rewrite prev_nth; case p_x: (x \in p) => //; case: p => [|y0 p] // in p_x *. by apply mem_nth; rewrite /= ltnS index_size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)