proposition: Lemma mem_next p x : (next p x \in p) = (x \in p).
proof: Proof. rewrite next_nth; case p_x: (x \in p) => //. case: p (index x p) p_x => [|y0 p'] //= i _; rewrite inE. have [lt_ip | ge_ip] := ltnP i (size p'); first by rewrite orbC mem_nth. by rewrite nth_default ?eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)