ι : Type ?u.141596
α : Type u_1
β : Type ?u.141602
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c
ι : Type ?u.141596
α : Type u_1
β : Type ?u.141602
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
no goals
ι : Type ?u.141596
α : Type u_1
β : Type ?u.141602
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c
exact sdiff_sdiff_le.trans le_sup_sdiff