Defaulted last-element lookup

The default is unused for a nonempty list. This indexed form follows from the core last-element lookup API.

Main results

• List.getLastD_eq_getElem.

theorem List.getLastD_eq_getElem {α : Type u_1} (xs : List α) (d : α) (hne : xs ≠ []) : xs.getLastD d = xs[xs.length - 1]

A nonempty list's defaulted last lookup is its final indexed element.