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.