Theorems · Theorem · order theory

add_tsub_add_le_tsub_left

∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b - (a + c) ≤ b - c

See add_tsub_add_eq_tsub_left for the equality.

Defined in

Mathlib.Algebra.Order.Sub.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderAddCommSemigroupSubOrderedSubAddLeftMono