how to avoid wrong detection of missing cases in match?

Stream: new members

[Stefan Kusterer]

def foo (n : Nat) (h : n ≤ 15) : String :=
  match n with
  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => s!"{n}"
  | 10 => "a"
  | 11 => "b"
  | 12 => "c"
  | 13 => "d"
  | 14 => "e"
  | 15 => "f"

works as expected (without any error) but the seemingly identical function

def fooo (n : Nat) (h : n < 16) : String :=
  match n with
  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => s!"{n}"
  | 10 => "a"
  | 11 => "b"
  | 12 => "c"
  | 13 => "d"
  | 14 => "e"
  | 15 => "f"

leads to error message

Missing cases:
(Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ _)))))))))))))))), _

Also adding unnecessary cases to the match-statement in fooo does not solve the issue.
Apparently, < works for number smaller than 16.
A similar question was raised in #new members > ✔ match on Fin ? @ 💬 for a similar situation.
Am I missing something? Is this a limitation that one should know about? ... or is this an issue?
Setup Information:

**Operating system**: Linux (release: 6.6.87.2-microsoft-standard-WSL2)
**CPU architecture**: x64
**CPU model**: 4 x Intel(R) Core(TM) i7-10510U CPU @ 1.80GHz
**Available RAM**: 16.77 GB

**VS Code version**: Reasonably up-to-date (version: 1.107.1)
**Lean 4 extension version**: 0.0.221
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.1.2)
**Lean**: Reasonably up-to-date (version: 4.26.0)
**Project**: Valid Lean project (path: /home/stefan/lean-numerals)
**Active Lean version**: leanprover/lean4:v4.26.0 (set by `file:///home/stefan/lean-numerals/lean-toolchain`)
**Installed Lean versions**: leanprover/lean4:v4.23.0, leanprover/lean4:v4.24.0, leanprover/lean4:v4.24.0-rc1, leanprover/lean4:v4.25.0, leanprover/lean4:v4.25.0-rc2, leanprover/lean4:v4.25.1, leanprover/lean4:v4.25.2, leanprover/lean4:v4.26.0, leanprover/lean4:v4.26.0-rc1, leanprover/lean4:v4.26.0-rc2, leanprover/lean4:v4.27.0-rc1

[JJ]

https://github.com/leanprover/lean4/issues/9292

[JJ]

relevant thread: #new members > ✔ what's up with numeric literals and Fin? @ 💬

[Stefan Kusterer]

JJ said:

https://github.com/leanprover/lean4/issues/9292

Thanks for pointing me to this issue, which seems not be caused by the use of Fin

[JJ]

yeah, the underlying issue appears to be in contradiction and match