feat(data/fin): last

Author: spl

data/fin.lean

@@ -6,6 +6,12 @@ namespace fin
 
 variable {n : ℕ}
 
+/-- The greatest value of `fin (n+1)` -/
+def last (n : ℕ) : fin (n+1) := ⟨_, n.lt_succ_self⟩
+
+theorem le_last (i : fin (n+1)) : i ≤ last n :=
+le_of_lt_succ i.is_lt
+
 /-- Embedding of `fin n` in `fin (n+1)` -/
 def raise (k : fin n) : fin (n + 1) := ⟨val k, lt_succ_of_lt (is_lt k)⟩