Theorems · Theorem · order theory

AddLECancellable.tsub_lt_self

∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, AddLECancellable a → 0 < a → 0 < b → a - b < a

Defined in

Mathlib.Algebra.Order.Sub.Basic

Cited by

3 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidLinearOrderCanonicallyOrderedAddSubOrderedSub