positivity and ENNReal

Stream: mathlib4

[Michael Stoll]

import Mathlib

example {n : ℕ} (hn : 0 < n) : (0 : ENNReal) < 1 / n := by
  positivity -- fails

Can positivity be taught to deal with this kind of goal? (I assume it needs to know that n is not infinity here.)
This came up when reviewing #16675.

[Yaël Dillies]

It can, especially now that we have the finiteness tactic

[Yury G. Kudryashov]

I plan to teach it to do that this weekend.