Could `norm_num` be extended to handle division in `NNReal`?

Stream: mathlib4

[Terence Tao]

Currently it seems that norm_num only handles division in division rings, excluding in particular NNReal? In the following example, I needed an ad hoc application of a Mathlib lemma to close:

import Mathlib

example : 1/10 < (1:NNReal) := by
  apply NNReal.div_lt_one_of_lt  -- necessary because `norm_num` does not work immediately
  norm_num

Tactics such as norm_cast, field_simp, and rify also did not work here.

[Eric Wieser]

#9915 fixes this and just needs review

[Jovan Gerbscheid]

bound seems to work:

import Mathlib

example : 1/10 < (1:NNReal) := by
  bound