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.

added 1 commit

• 13ed6a8d - Applied suggested changes

Compare with previous version

resolved all threads

resolved all threads

changed title from Added [last_cons_ne] lemma for the [last] function to Add{+ +}last_cons_{+Some_+}ne{++} lemma for the {++}last{++} function

enabled an automatic merge when the pipeline for 13ed6a8d succeeds

Merging.

merged

mentioned in commit e58dd720