no goals
α : Type ?u.816967
β : Type ?u.816970
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]