norm_num can't prove 1 / 2 < 1

Stream: mathlib4

[Violeta Hernández]

...in NNReal:

import Mathlib

example : (2 : NNReal)⁻¹ < 1 := by
  norm_num -- fails

[Violeta Hernández]

Is this expected behavior, or is it a bug?

[Ruben Van de Velde]

The "in NNReal" is probably the issue, yeah. Looks like there's a WIP from @Eric Wieser at https://github.com/leanprover-community/mathlib4/pull/9915