no goals
α : Type ?u.794102
β : Type ?u.794105
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_eq_coe,
  Real.toNNReal_add hp hq]