proposition: Lemma next_prev : cancel (prev p) (next p).
proof: Proof. move=> x; rewrite next_nth mem_prev prev_nth; case p_x: (x \in p) => //. case def_p: p p_x => // [y q]; rewrite -def_p => p_x. rewrite index_uniq //; last by rewrite def_p ltnS index_size. case q_x: (x \in q); first exact: nth_index. rewrite nth_default; last by rewrite leqNgt index_mem q_x. by apply/eqP; rewrite def_p inE q_x orbF eq_sym in p_x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)