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