WithTop.sub_top

theorem WithTop.sub_top : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Zero α] {a : WithTop α}, a - ⊤ = 0

The theorem `WithTop.sub_top` states that for any type `α` that has subtraction (`Sub α`) and zero (`Zero α`) operations defined, subtracting the top element `⊤` from any element `a` of the type `WithTop α` (which is essentially the type `α` augmented with an additional top element `⊤`), will always result in zero. This theorem is valid irrespective of the specific element `a` chosen from the `WithTop α` type.

More concisely: For any type `α` with subtraction and zero operations, `⊤ - a = Zero α` for all `a` in `WithTop α`.