simp
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ^ p ≠ ⊤
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.toReal a ≤ 0 → 0 ≤ p