. rw [add_comm]
  refine ENNReal.lt_add_right ?_ ?_
  . rw [← lt_top_iff_ne_top]
    simp
    exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
  . rwa [ENNReal.inv_ne_zero]
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹
no goals