Added some useful lemmas for the [last] function

Added some utility lemmas for the [last] function. (precursor to the !353 (merged) MR)

added 1 commit

• 87eb1296 - Added explicit names of variables for induction tactic

Compare with previous version

added 1 commit

• dd560b2c - Renamed [last_filter_lookup] to [last_Some_elem_of] and refactored

Compare with previous version

added 1 commit

• 168b1aaf - More refactoring

Compare with previous version

resolved all threads

LGTM. You want to add a changelog entry? Since the theory of last has been quite underdeveloped, it might be worth pointing this out.

added 1 commit

• 5f4e67b1 - Added a changelog note about the new lemmas for [last]

Compare with previous version

approved this merge request

added 1 commit

• dcf47357 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for dcf47357 succeeds

Merging. Thanks.

merged

mentioned in commit 50117aa6