ι : Type ?u.142580
α : Type u_1
β : Type ?u.142586
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c
ι : Type ?u.142580
α : Type u_1
β : Type ?u.142586
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c
rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
no goals
ι : Type ?u.142580
α : Type u_1
β : Type ?u.142586
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c
exact sdiff_le_sdiff_right h