Checked Non-Terminating Recursive Def?

The following appears to type check in Lean 4:

def len_succ {a:Type} (h:a)(t:List a) : (h::t).length = t.length+1  :=
by
  induction t
  repeat simp

def pop {a:Type} (st:List a)(n:Nat)(r:n <= st.length) : List a :=
  match st with
  | h::t =>
      pop t (n-1) (by
        rw [Nat.sub_le_iff_le_add]
        rw [<- len_succ h t]
        exact r
  )
  | [] => []

I feel confused about this, given that n-1 can underflow. Did I miss something?

In the natural numbers in Lean, subtraction is "truncating", so in particular 0 - 1 = 0.