ι : Type ?u.94869
α : Type u_1
β : Type ?u.94875
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a ⊔ (b ⊔ c)
ι : Type ?u.94869
α : Type u_1
β : Type ?u.94875
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ (a \ c) ≤ c \ b
rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
  sup_left_comm]
no goals
ι : Type ?u.94869
α : Type u_1
β : Type ?u.94875
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a ⊔ (b ⊔ c)
exact le_sup_left