proposition: Lemma prev_next : cancel (next p) (prev p).
proof: Proof. move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //. case Dp: p Up p_x => // [y q]; rewrite [uniq _]/= -Dp => /andP[q'y Uq] p_x. rewrite -[RHS](nth_index y p_x); congr (nth y _ _); set i := index x p. have: i <= size q by rewrite -index_mem -/i Dp in p_x. case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq. by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)