α : Type u_1
β : Type ?u.40621
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False
α : Type u_1
β : Type ?u.40621
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a + c < b
⊢ a ≠ b - c
rintro rfl
no goals
α : Type u_1
β : Type ?u.40621
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False
exact h.not_le le_tsub_add