chore(positivity): tests for two more extensions (leanprover-community#37511)

I believe these extensions are not explicitly tested yet: I've added one as I wondered about this today.

Author: grunweg

MathlibTest/positivity.lean

@@ -286,6 +286,9 @@ example (ha : a ≠ 0) : 0 < a * 37 := by positivity
 example (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b := by positivity
 example (ha : a ≠ 0) : 0 ≤ a * b := by positivity
 
+example : 0 ≤ a.toReal := by positivity
+example {a' : ℝ≥0} : 0 ≤ ENNReal.ofNNReal a' := by positivity
+
 /- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Adding.20superfluous.20hypotheses.20makes.20positivity.20fail/with/568774307 -/
 example {x y : ℝ≥0∞} : x + y + 1 ≠ 0 := by positivity
 example {x y : ℝ≥0∞} (hx : x ≠ 0) : x + y + 1 ≠ 0 := by positivity