Commit 2024-10-03 20:47 aeefd817
View on Github →refactor: Let positivity handle ENNReal-valued ofNat (#17212)
The meta code was looking for StrictOrderedSemiring instead of the weaker OrderedSemiring + Nontrivial, which is enough.
From LeanAPAP