List.modifyLast

theorem List.modifyLast_concat {α : Type u_1} (f : α → α) (a : α) (l : List α) : modifyLast f (l ++ [a]) = l ++ [f a]

theorem List.modifyLast_append_of_right_ne_nil {α : Type u_1} (f : α → α) (l₁ l₂ : List α) : l₂ ≠ [] → modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂