## Stream: general

### Topic: nth_le

#### Kenny Lau (Jul 27 2018 at 07:32):

@[simp] def nth_le : Π (l : list α) (n), n < l.length → α
| []       n     h := absurd h (not_lt_zero n)
| (a :: l) 0     h := a
| (a :: l) (n+1) h := nth_le l n (le_of_succ_le_succ h)


So why exactly is this called nth_le?

Last updated: May 14 2021 at 07:19 UTC