Lean4
/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the previous
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.
* `prev [1, 2, 3] 2 _ = 1`
* `prev [1, 2, 3] 1 _ = 3`
* `prev [1, 2, 3, 2, 4] 2 _ = 1`
* `prev [1, 2, 3, 4, 2] 2 _ = 1`
* `prev [1, 1, 2] 1 _ = 2`
-/
def prev : ∀ l : List α, ∀ x ∈ l, α
| [], _, h => by simp at h
| [y], _, _ => y
| y :: z :: xs, x, h =>
if hx : x = y then getLast (z :: xs) (cons_ne_nil _ _)
else if x = z then y else prev (z :: xs) x (by simpa [hx] using h)
