# Add `last_cons_Some_ne` lemma for the `last` function

A useful lemma for the [last] function, to reduce `last (x::l) = Some y`

to `last l = Some y`

whenever `x ≠ y`

.
This is useful since using `last_cons`

leaves us with

```
match last l with
| Some y0 => Some y0
| None => Some x
end = Some y
```

which only reduces through a subgoal.

Edited by Robbert Krebbers