no goals
ι : Type ?u.32704
α : Type u_1
β : Type ?u.32710
π : ι → Type ?u.32715
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) ∆ b = a ⊔ b
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]