Defaulted last-element lookup

The default is unused for a nonempty list. This indexed form follows from the core last-element lookup API. The default of an append is threaded through its left part, which is how the endpoint of a concatenated walk is computed.

Main results

• List.getLastD_eq_getElem.
• List.getLastD_append.

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.

theorem List.getLastD_append {α : Type u_1} (l₁ l₂ : List α) (d : α) : (l₁ ++ l₂).getLastD d = l₂.getLastD (l₁.getLastD d)

The defaulted last element of an append: the right part's, with the left part's as default.