proposition: Lemma prev_nth p x : prev 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; rewrite inE orbC. elim: p {2 5}y0 => [|y' p IHp] y; rewrite /= ?inE // (eq_sym y'). by case: ifP => // _; apply: IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)