proposition: Lemma next_nth p x : next p x = if x \in p then if p is y :: p' then nth y p' (index x p) else x else x.
proof: Proof. case: p => //= y0 p. elim: p {2 3 5}y0 => [|y' p IHp] y /=; rewrite (eq_sym y) inE; by case: ifP => // _; apply: IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)