α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b
refine'
  ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne _⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b
rintro rfl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a < a
⊢ False
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False
rw [tsub_zero] at h
no goals
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a < a
⊢ False
exact h.false