Lemmas about Fin.clamp

theorem Fin.clamp_monotone {m : ℕ} : Monotone fun (n : ℕ) => clamp n m

theorem Fin.clamp_eq_last (n m : ℕ) (hmn : m ≤ n) : clamp n m = last m