no goals
ι : Type ?u.20047
α : Type u_1
β : Type ?u.20053
π : ι → Type ?u.20058
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a ∆ b = b \ a
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]