no goals
α : Type u_1
β : Type ?u.2076
inst✝¹ : Sub α
inst✝ : Zero α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
induction a using recTopCoe <;> induction b using recTopCoe <;>
  simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and,
    Ne.def]