no goals
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 / ENNReal.ofReal p + 1 / ENNReal.ofReal q = 1
rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_div_of_pos h.pos,
    ← ENNReal.ofReal_div_of_pos h.symm.pos,
    ← ENNReal.ofReal_add h.one_div_nonneg h.symm.one_div_nonneg, h.inv_add_inv_conj]