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