. intro h
  suffices hba : b ≤ a
  . simpa [← ENNReal.sub_right_inj ha' hba]
  have hba : 0 < a - b
  . simpa [h, zero_lt_iff]
  simp at hba
  exact hba.le
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0

case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a