doc-next-gen

Mathlib.Algebra.Order.Sub.Defs

Module docstring

{"# Ordered Subtraction

This file proves lemmas relating (truncated) subtraction with an order. We provide a class OrderedSub stating that a - b ≤ c ↔ a ≤ c + b.

The subtraction discussed here could both be normal subtraction in an additive group or truncated subtraction on a canonically ordered monoid (ℕ, Multiset, PartENat, ENNReal, ...)

Implementation details

OrderedSub is a mixin type-class, so that we can use the results in this file even in cases where we don't have a CanonicallyOrderedAdd instance (even though that is our main focus). Conversely, this means we can use CanonicallyOrderedAdd without necessarily having to define a subtraction.

The results in this file are ordered by the type-class assumption needed to prove it. This means that similar results might not be close to each other. Furthermore, we don't prove implications if a bi-implication can be proven under the same assumptions.

Lemmas using this class are named using tsub instead of sub (short for \"truncated subtraction\"). This is to avoid naming conflicts with similar lemmas about ordered groups.

We provide a second version of most results that require [AddLeftReflectLE α]. In the second version we replace this type-class assumption by explicit AddLECancellable assumptions.

TODO: maybe we should make a multiplicative version of this, so that we can replace some identical lemmas about subtraction/division in Ordered[Add]CommGroup with these.

TODO: generalize Nat.le_of_le_of_sub_le_sub_right, Nat.sub_le_sub_right_iff, Nat.mul_self_sub_mul_self_eq ","### Preorder ","#### Lemmas that assume that an element is AddLECancellable ","### Lemmas where addition is order-reflecting ","### Partial order ","### Lemmas that assume that an element is AddLECancellable. ","#### Lemmas where addition is order-reflecting. ","### Lemmas in a linearly ordered monoid. "}

OrderedSub structure
(α : Type*) [LE α] [Add α] [Sub α]
Full source 
/-- `OrderedSub α` means that `α` has a subtraction characterized by `a - b ≤ c ↔ a ≤ c + b`.
In other words, `a - b` is the least `c` such that `a ≤ b + c`.

This is satisfied both by the subtraction in additive ordered groups and by truncated subtraction
in canonically ordered monoids on many specific types.
-/
class OrderedSub (α : Type*) [LE α] [Add α] [Sub α] : Prop where
  /-- `a - b` provides a lower bound on `c` such that `a ≤ c + b`. -/
  tsub_le_iff_right : ∀ a b c : α, a - b ≤ c ↔ a ≤ c + b
Ordered Subtraction Structure
Informal description
The structure `OrderedSub α` characterizes a type `α` with a subtraction operation `-` and an addition operation `+` that satisfy the property: for any elements `a, b, c ∈ α`, the inequality `a - b ≤ c` holds if and only if `a ≤ c + b`. This means `a - b` is the smallest element `c` such that `a ≤ b + c`. This property is satisfied both by: 1. Subtraction in additive ordered groups 2. Truncated subtraction in canonically ordered monoids (like `ℕ`, `Multiset`, `PartENat`, `ENNReal`, etc.)
tsub_le_iff_right theorem
[LE α] [Add α] [Sub α] [OrderedSub α] {a b c : α} : a - b ≤ c ↔ a ≤ c + b
Full source 
@[simp]
theorem tsub_le_iff_right [LE α] [Add α] [Sub α] [OrderedSub α] {a b c : α} :
    a - b ≤ c ↔ a ≤ c + b :=
  OrderedSub.tsub_le_iff_right a b c
Characterization of Ordered Subtraction: $a - b \leq c \leftrightarrow a \leq c + b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - b \leq c$ holds if and only if $a \leq c + b$.
add_tsub_le_right theorem
: a + b - b ≤ a
Full source 
/-- See `add_tsub_cancel_right` for the equality if `AddLeftReflectLE α`. -/
theorem add_tsub_le_right : a + b - b ≤ a :=
  tsub_le_iff_right.mpr le_rfl
Subtraction Inequality: $(a + b) - b \leq a$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $(a + b) - b \leq a$.
le_tsub_add theorem
: b ≤ b - a + a
Full source 
theorem le_tsub_add : b ≤ b - a + a :=
  tsub_le_iff_right.mp le_rfl
Subtraction-Addition Inequality: $b \leq (b - a) + a$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $b \leq (b - a) + a$.
tsub_le_iff_left theorem
: a - b ≤ c ↔ a ≤ b + c
Full source 
theorem tsub_le_iff_left : a - b ≤ c ↔ a ≤ b + c := by rw [tsub_le_iff_right, add_comm]
Characterization of Ordered Subtraction: $a - b \leq c \leftrightarrow a \leq b + c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - b \leq c$ holds if and only if $a \leq b + c$.
le_add_tsub theorem
: a ≤ b + (a - b)
Full source 
theorem le_add_tsub : a ≤ b + (a - b) :=
  tsub_le_iff_left.mp le_rfl
Subtraction-Addition Inequality: $a \leq b + (a - b)$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $a \leq b + (a - b)$.
add_tsub_le_left theorem
: a + b - a ≤ b
Full source 
/-- See `add_tsub_cancel_left` for the equality if `AddLeftReflectLE α`. -/
theorem add_tsub_le_left : a + b - a ≤ b :=
  tsub_le_iff_left.mpr le_rfl
Subtraction Inequality: $(a + b) - a \leq b$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $(a + b) - a \leq b$.
tsub_le_tsub_right theorem
(h : a ≤ b) (c : α) : a - c ≤ b - c
Full source 
@[gcongr] theorem tsub_le_tsub_right (h : a ≤ b) (c : α) : a - c ≤ b - c :=
  tsub_le_iff_left.mpr <| h.trans le_add_tsub
Right Subtraction Preserves Order: $a \leq b \Rightarrow a - c \leq b - c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a \leq b$, then $a - c \leq b - c$.
tsub_le_iff_tsub_le theorem
: a - b ≤ c ↔ a - c ≤ b
Full source 
theorem tsub_le_iff_tsub_le : a - b ≤ c ↔ a - c ≤ b := by rw [tsub_le_iff_left, tsub_le_iff_right]
Subtraction Order Equivalence: $a - b \leq c \leftrightarrow a - c \leq b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - b \leq c$ holds if and only if $a - c \leq b$.
tsub_tsub_le theorem
: b - (b - a) ≤ a
Full source 
/-- See `tsub_tsub_cancel_of_le` for the equality. -/
theorem tsub_tsub_le : b - (b - a) ≤ a :=
  tsub_le_iff_right.mpr le_add_tsub
Double Subtraction Inequality: $b - (b - a) \leq a$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $b - (b - a) \leq a$.
tsub_le_tsub_left theorem
(h : a ≤ b) (c : α) : c - b ≤ c - a
Full source 
@[gcongr] theorem tsub_le_tsub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
  tsub_le_iff_left.mpr <| le_add_tsub.trans <| add_le_add_right h _
Monotonicity of Subtraction in the Second Argument: $a \leq b \Rightarrow c - b \leq c - a$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a \leq b$, then $c - b \leq c - a$ for any $c \in \alpha$.
tsub_le_tsub theorem
(hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c
Full source 
@[gcongr] theorem tsub_le_tsub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
  (tsub_le_tsub_right hab _).trans <| tsub_le_tsub_left hcd _
Subtraction Preserves Order: $a \leq b \land c \leq d \Rightarrow a - d \leq b - c$
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a \leq b$ and $c \leq d$, then $a - d \leq b - c$.
antitone_const_tsub theorem
: Antitone fun x => c - x
Full source 
theorem antitone_const_tsub : Antitone fun x => c - x := fun _ _ hxy => tsub_le_tsub rfl.le hxy
Antitonicity of Constant Subtraction: $x \mapsto c - x$ is antitone
Informal description
For any element $c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the function $x \mapsto c - x$ is antitone. That is, for any $x, y \in \alpha$, if $x \leq y$, then $c - y \leq c - x$.
add_tsub_le_assoc theorem
: a + b - c ≤ a + (b - c)
Full source 
/-- See `add_tsub_assoc_of_le` for the equality. -/
theorem add_tsub_le_assoc : a + b - c ≤ a + (b - c) := by
  rw [tsub_le_iff_left, add_left_comm]
  exact add_le_add_left le_add_tsub a
Associative Inequality for Ordered Subtraction: $(a + b) - c \leq a + (b - c)$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $(a + b) - c \leq a + (b - c)$ holds.
add_tsub_le_tsub_add theorem
: a + b - c ≤ a - c + b
Full source 
/-- See `tsub_add_eq_add_tsub` for the equality. -/
theorem add_tsub_le_tsub_add : a + b - c ≤ a - c + b := by
  rw [add_comm, add_comm _ b]
  exact add_tsub_le_assoc
Subtraction-Additive Inequality: $(a + b) - c \leq (a - c) + b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $(a + b) - c \leq (a - c) + b$ holds.
add_le_add_add_tsub theorem
: a + b ≤ a + c + (b - c)
Full source 
theorem add_le_add_add_tsub : a + b ≤ a + c + (b - c) := by
  rw [add_assoc]
  exact add_le_add_left le_add_tsub a
Addition-Subtraction Inequality: $a + b \leq a + c + (b - c)$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $a + b \leq a + c + (b - c)$.
le_tsub_add_add theorem
: a + b ≤ a - c + (b + c)
Full source 
theorem le_tsub_add_add : a + b ≤ a - c + (b + c) := by
  rw [add_comm a, add_comm (a - c)]
  exact add_le_add_add_tsub
Subtraction-Addition Inequality: $a + b \leq (a - c) + (b + c)$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, we have $a + b \leq (a - c) + (b + c)$.
tsub_le_tsub_add_tsub theorem
: a - c ≤ a - b + (b - c)
Full source 
theorem tsub_le_tsub_add_tsub : a - c ≤ a - b + (b - c) := by
  rw [tsub_le_iff_left, ← add_assoc, add_right_comm]
  exact le_add_tsub.trans (add_le_add_right le_add_tsub _)
Subtraction Triangle Inequality: $a - c \leq (a - b) + (b - c)$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - c \leq (a - b) + (b - c)$ holds.
tsub_tsub_tsub_le_tsub theorem
: c - a - (c - b) ≤ b - a
Full source 
theorem tsub_tsub_tsub_le_tsub : c - a - (c - b) ≤ b - a := by
  rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm]
  exact le_tsub_add.trans (add_le_add_left le_add_tsub _)
Subtraction Triple Inequality: $(c - a) - (c - b) \leq b - a$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $(c - a) - (c - b) \leq b - a$ holds.
tsub_tsub_le_tsub_add theorem
{a b c : α} : a - (b - c) ≤ a - b + c
Full source 
theorem tsub_tsub_le_tsub_add {a b c : α} : a - (b - c) ≤ a - b + c :=
  tsub_le_iff_right.2 <|
    calc
      a ≤ a - b + b := le_tsub_add
      _ ≤ a - b + (c + (b - c)) := add_le_add_left le_add_tsub _
      _ = a - b + c + (b - c) := (add_assoc _ _ _).symm
Subtraction Chain Inequality: $a - (b - c) \leq a - b + c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - (b - c) \leq a - b + c$ holds.
add_tsub_add_le_tsub_add_tsub theorem
: a + b - (c + d) ≤ a - c + (b - d)
Full source 
/-- See `tsub_add_tsub_comm` for the equality. -/
theorem add_tsub_add_le_tsub_add_tsub : a + b - (c + d) ≤ a - c + (b - d) := by
  rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
  refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_
  rw [add_comm a, add_comm (a - c)]
  exact add_tsub_le_assoc
Subtraction-Additive Inequality: $(a + b) - (c + d) \leq (a - c) + (b - d)$
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with ordered subtraction, the inequality $(a + b) - (c + d) \leq (a - c) + (b - d)$ holds.
add_tsub_add_le_tsub_left theorem
: a + b - (a + c) ≤ b - c
Full source 
/-- See `add_tsub_add_eq_tsub_left` for the equality. -/
theorem add_tsub_add_le_tsub_left : a + b - (a + c) ≤ b - c := by
  rw [tsub_le_iff_left, add_assoc]
  exact add_le_add_left le_add_tsub _
Left Addition-Subtraction Inequality: $(a + b) - (a + c) \leq b - c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ with ordered subtraction, the inequality $(a + b) - (a + c) \leq b - c$ holds.
add_tsub_add_le_tsub_right theorem
: a + c - (b + c) ≤ a - b
Full source 
/-- See `add_tsub_add_eq_tsub_right` for the equality. -/
theorem add_tsub_add_le_tsub_right : a + c - (b + c) ≤ a - b := by
  rw [tsub_le_iff_left, add_right_comm]
  exact add_le_add_right le_add_tsub c
Right Cancellation Inequality for Ordered Subtraction: $(a + c) - (b + c) \leq a - b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $(a + c) - (b + c) \leq a - b$ holds.
AddLECancellable.le_add_tsub_swap theorem
(hb : AddLECancellable b) : a ≤ b + a - b
Full source 
protected theorem le_add_tsub_swap (hb : AddLECancellable b) : a ≤ b + a - b :=
  hb le_add_tsub
Additive Cancellability Implies $a \leq b + a - b$
Informal description
For any elements $a, b$ in a type $\alpha$ with ordered subtraction, if $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$), then $a \leq b + a - b$.
AddLECancellable.le_add_tsub theorem
(hb : AddLECancellable b) : a ≤ a + b - b
Full source 
protected theorem le_add_tsub (hb : AddLECancellable b) : a ≤ a + b - b := by
  rw [add_comm]
  exact hb.le_add_tsub_swap
Additive Cancellability Implies $a \leq a + b - b$
Informal description
For any elements $a, b$ in a type $\alpha$ with ordered subtraction, if $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$), then $a \leq a + b - b$.
AddLECancellable.le_tsub_of_add_le_left theorem
(ha : AddLECancellable a) (h : a + b ≤ c) : b ≤ c - a
Full source 
protected theorem le_tsub_of_add_le_left (ha : AddLECancellable a) (h : a + b ≤ c) : b ≤ c - a :=
  ha <| h.trans le_add_tsub
Left Cancellable Addition Implies Subtraction Inequality: $a + b \leq c \Rightarrow b \leq c - a$
Informal description
Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$) and $a + b \leq c$, then $b \leq c - a$.
AddLECancellable.le_tsub_of_add_le_right theorem
(hb : AddLECancellable b) (h : a + b ≤ c) : a ≤ c - b
Full source 
protected theorem le_tsub_of_add_le_right (hb : AddLECancellable b) (h : a + b ≤ c) : a ≤ c - b :=
  hb.le_tsub_of_add_le_left <| by rwa [add_comm]
Right Cancellable Addition Implies Subtraction Inequality: $a + b \leq c \Rightarrow a \leq c - b$
Informal description
Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $b$ is additively left cancellable (i.e., $x + b \leq y + b$ implies $x \leq y$) and $a + b \leq c$, then $a \leq c - b$.
le_add_tsub_swap theorem
: a ≤ b + a - b
Full source 
theorem le_add_tsub_swap : a ≤ b + a - b :=
  Contravariant.AddLECancellable.le_add_tsub_swap
Inequality for Ordered Subtraction: $a \leq b + a - b$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with ordered subtraction, it holds that $a \leq b + a - b$.
le_add_tsub' theorem
: a ≤ a + b - b
Full source 
theorem le_add_tsub' : a ≤ a + b - b :=
  Contravariant.AddLECancellable.le_add_tsub
Inequality for Ordered Subtraction: $a \leq a + b - b$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with ordered subtraction, it holds that $a \leq a + b - b$.
le_tsub_of_add_le_left theorem
(h : a + b ≤ c) : b ≤ c - a
Full source 
theorem le_tsub_of_add_le_left (h : a + b ≤ c) : b ≤ c - a :=
  Contravariant.AddLECancellable.le_tsub_of_add_le_left h
Subtraction Inequality from Left Addition: $a + b \leq c \Rightarrow b \leq c - a$
Informal description
For any elements $a, b, c$ in a type $\alpha$ with ordered subtraction, if $a + b \leq c$, then $b \leq c - a$.
le_tsub_of_add_le_right theorem
(h : a + b ≤ c) : a ≤ c - b
Full source 
theorem le_tsub_of_add_le_right (h : a + b ≤ c) : a ≤ c - b :=
  Contravariant.AddLECancellable.le_tsub_of_add_le_right h
Subtraction Inequality from Right Addition: $a + b \leq c \Rightarrow a \leq c - b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ with ordered subtraction, if $a + b \leq c$, then $a \leq c - b$.
tsub_nonpos theorem
: a - b ≤ 0 ↔ a ≤ b
Full source 
theorem tsub_nonpos : a - b ≤ 0 ↔ a ≤ b := by rw [tsub_le_iff_left, add_zero]
Characterization of Nonpositive Subtraction: $a - b \leq 0 \leftrightarrow a \leq b$
Informal description
For any elements $a, b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a - b \leq 0$ holds if and only if $a \leq b$.
tsub_tsub theorem
(b a c : α) : b - a - c = b - (a + c)
Full source 
theorem tsub_tsub (b a c : α) : b - a - c = b - (a + c) := by
  apply le_antisymm
  · rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
  · rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
Subtraction Composition Identity: $(b - a) - c = b - (a + c)$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with addition $+$ and subtraction $-$ satisfying the `OrderedSub` property, the equality $(b - a) - c = b - (a + c)$ holds.
tsub_add_eq_tsub_tsub theorem
(a b c : α) : a - (b + c) = a - b - c
Full source 
theorem tsub_add_eq_tsub_tsub (a b c : α) : a - (b + c) = a - b - c :=
  (tsub_tsub _ _ _).symm
Subtraction of Sum: $a - (b + c) = a - b - c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with addition $+$ and subtraction $-$ satisfying the `OrderedSub` property, the equality $a - (b + c) = a - b - c$ holds.
tsub_add_eq_tsub_tsub_swap theorem
(a b c : α) : a - (b + c) = a - c - b
Full source 
theorem tsub_add_eq_tsub_tsub_swap (a b c : α) : a - (b + c) = a - c - b := by
  rw [add_comm]
  apply tsub_add_eq_tsub_tsub
Subtraction of Sum with Swapped Order: $a - (b + c) = a - c - b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with addition $+$ and subtraction $-$ satisfying the `OrderedSub` property, the equality $a - (b + c) = a - c - b$ holds.
tsub_right_comm theorem
: a - b - c = a - c - b
Full source 
theorem tsub_right_comm : a - b - c = a - c - b := by
  rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]
Right Commutativity of Subtraction: $a - b - c = a - c - b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with subtraction $-$ satisfying the `OrderedSub` property, the equality $a - b - c = a - c - b$ holds.
AddLECancellable.tsub_eq_of_eq_add theorem
(hb : AddLECancellable b) (h : a = c + b) : a - b = c
Full source 
/-- See `AddLECancellable.tsub_eq_of_eq_add'` for a version assuming that `a = c + b` itself is
cancellable rather than `b`. -/
protected theorem tsub_eq_of_eq_add (hb : AddLECancellable b) (h : a = c + b) : a - b = c :=
  le_antisymm (tsub_le_iff_right.mpr h.le) <| by
    rw [h]
    exact hb.le_add_tsub
Subtraction from Cancellable Addition: $a = c + b$ implies $a - b = c$ when $b$ is cancellable
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$) and $a = c + b$, then $a - b = c$.
AddLECancellable.tsub_eq_of_eq_add' theorem
[AddLeftMono α] (ha : AddLECancellable a) (h : a = c + b) : a - b = c
Full source 
/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add` assuming that `a = c + b` itself is
cancellable rather than `b`. -/
protected lemma tsub_eq_of_eq_add' [AddLeftMono α] (ha : AddLECancellable a)
    (h : a = c + b) : a - b = c := (h ▸ ha).of_add_right.tsub_eq_of_eq_add h
Subtraction from Cancellable Addition (variant): $a = c + b$ implies $a - b = c$ when $a$ is cancellable
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$) and $a = c + b$, then $a - b = c$.
AddLECancellable.tsub_eq_of_eq_add_rev theorem
(hb : AddLECancellable b) (h : a = b + c) : a - b = c
Full source 
/-- See `AddLECancellable.tsub_eq_of_eq_add_rev'` for a version assuming that `a = b + c` itself is
cancellable rather than `b`. -/
protected theorem tsub_eq_of_eq_add_rev (hb : AddLECancellable b) (h : a = b + c) : a - b = c :=
  hb.tsub_eq_of_eq_add <| by rw [add_comm, h]
Subtraction from Cancellable Addition: $a = b + c$ implies $a - b = c$ when $b$ is cancellable
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$) and $a = b + c$, then $a - b = c$.
AddLECancellable.tsub_eq_of_eq_add_rev' theorem
[AddLeftMono α] (ha : AddLECancellable a) (h : a = b + c) : a - b = c
Full source 
/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add_rev` assuming that `a = b + c` itself is
cancellable rather than `b`. -/
protected lemma tsub_eq_of_eq_add_rev' [AddLeftMono α]
    (ha : AddLECancellable a) (h : a = b + c) : a - b = c :=
  ha.tsub_eq_of_eq_add' <| by rw [add_comm, h]
Subtraction from Cancellable Addition (order-reflecting variant): $a = b + c$ implies $a - b = c$ when $a$ is cancellable
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if addition is order-reflecting (i.e., $x + y \leq x + z$ implies $y \leq z$ for all $x, y, z$), $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$), and $a = b + c$, then $a - b = c$.
AddLECancellable.add_tsub_cancel_right theorem
(hb : AddLECancellable b) : a + b - b = a
Full source 
@[simp]
protected theorem add_tsub_cancel_right (hb : AddLECancellable b) : a + b - b = a :=
  hb.tsub_eq_of_eq_add <| by rw [add_comm]
Cancellable Right Subtraction: $(a + b) - b = a$ when $b$ is cancellable
Informal description
For any elements $a, b$ in a type $\alpha$ with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$), then $(a + b) - b = a$.
AddLECancellable.add_tsub_cancel_left theorem
(ha : AddLECancellable a) : a + b - a = b
Full source 
@[simp]
protected theorem add_tsub_cancel_left (ha : AddLECancellable a) : a + b - a = b :=
  ha.tsub_eq_of_eq_add <| add_comm a b
Cancellable Left Subtraction: $(a + b) - a = b$ when $a$ is cancellable
Informal description
For any elements $a, b$ in a type $\alpha$ with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$), then $(a + b) - a = b$.
AddLECancellable.lt_add_of_tsub_lt_left theorem
(hb : AddLECancellable b) (h : a - b < c) : a < b + c
Full source 
protected theorem lt_add_of_tsub_lt_left (hb : AddLECancellable b) (h : a - b < c) : a < b + c := by
  rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
  refine ⟨h.le, ?_⟩
  rintro rfl
  simp [hb] at h
Strict Inequality from Truncated Subtraction Under Cancellable Addition: $a - b < c \Rightarrow a < b + c$
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$) and $a - b < c$, then $a < b + c$.
AddLECancellable.lt_add_of_tsub_lt_right theorem
(hc : AddLECancellable c) (h : a - c < b) : a < b + c
Full source 
protected theorem lt_add_of_tsub_lt_right (hc : AddLECancellable c) (h : a - c < b) :
    a < b + c := by
  rw [lt_iff_le_and_ne, ← tsub_le_iff_right]
  refine ⟨h.le, ?_⟩
  rintro rfl
  simp [hc] at h
Strict Addition Inequality Under Cancellable Subtraction: $a - c < b \Rightarrow a < b + c$
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $c$ is additively left cancellable (i.e., $x + c \leq y + c$ implies $x \leq y$) and $a - c < b$, then $a < b + c$.
AddLECancellable.lt_tsub_of_add_lt_right theorem
(hc : AddLECancellable c) (h : a + c < b) : a < b - c
Full source 
protected theorem lt_tsub_of_add_lt_right (hc : AddLECancellable c) (h : a + c < b) : a < b - c :=
  (hc.le_tsub_of_add_le_right h.le).lt_of_ne <| by
    rintro rfl
    exact h.not_le le_tsub_add
Strict Subtraction Inequality Under Cancellable Addition: $a + c < b \Rightarrow a < b - c$
Informal description
Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $c$ is additively left cancellable (i.e., $x + c \leq y + c$ implies $x \leq y$) and $a + c < b$, then $a < b - c$.
AddLECancellable.lt_tsub_of_add_lt_left theorem
(ha : AddLECancellable a) (h : a + c < b) : c < b - a
Full source 
protected theorem lt_tsub_of_add_lt_left (ha : AddLECancellable a) (h : a + c < b) : c < b - a :=
  ha.lt_tsub_of_add_lt_right <| by rwa [add_comm]
Strict Subtraction Inequality Under Left Cancellable Addition: $a + c < b \Rightarrow c < b - a$
Informal description
Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. If $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$) and $a + c < b$, then $c < b - a$.
tsub_eq_of_eq_add theorem
(h : a = c + b) : a - b = c
Full source 
theorem tsub_eq_of_eq_add (h : a = c + b) : a - b = c :=
  Contravariant.AddLECancellable.tsub_eq_of_eq_add h
Subtraction from Addition: $a = c + b$ implies $a - b = c$
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if $a = c + b$, then $a - b = c$.
tsub_eq_of_eq_add_rev theorem
(h : a = b + c) : a - b = c
Full source 
theorem tsub_eq_of_eq_add_rev (h : a = b + c) : a - b = c :=
  Contravariant.AddLECancellable.tsub_eq_of_eq_add_rev h
Subtraction from Addition: $a = b + c$ implies $a - b = c$
Informal description
Let $\alpha$ be a type with a preorder $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. For any elements $a, b, c \in \alpha$, if $a = b + c$, then $a - b = c$.
add_tsub_cancel_right theorem
(a b : α) : a + b - b = a
Full source 
@[simp]
theorem add_tsub_cancel_right (a b : α) : a + b - b = a :=
  Contravariant.AddLECancellable.add_tsub_cancel_right
Right Subtraction Cancellation: $(a + b) - b = a$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the equality $(a + b) - b = a$ holds.
add_tsub_cancel_left theorem
(a b : α) : a + b - a = b
Full source 
@[simp]
theorem add_tsub_cancel_left (a b : α) : a + b - a = b :=
  Contravariant.AddLECancellable.add_tsub_cancel_left
Left Subtraction Cancellation: $(a + b) - a = b$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the equality $(a + b) - a = b$ holds.
tsub_eq_tsub_of_add_eq_add theorem
(h : a + d = c + b) : a - b = c - d
Full source 
/-- A more general version of the reverse direction of `sub_eq_sub_iff_add_eq_add` -/
theorem tsub_eq_tsub_of_add_eq_add (h : a + d = c + b) : a - b = c - d := by
  calc a - b = a + d - d - b := by rw [add_tsub_cancel_right]
           _ = c + b - b - d := by rw [h, tsub_right_comm]
           _ = c - d := by rw [add_tsub_cancel_right]
Subtraction Equality under Addition Equality: $a + d = c + b \Rightarrow a - b = c - d$
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a + d = c + b$, then $a - b = c - d$.
lt_add_of_tsub_lt_left theorem
(h : a - b < c) : a < b + c
Full source 
theorem lt_add_of_tsub_lt_left (h : a - b < c) : a < b + c :=
  Contravariant.AddLECancellable.lt_add_of_tsub_lt_left h
Strict Inequality from Truncated Subtraction: $a - b < c \Rightarrow a < b + c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ with a preorder $\leq$, addition $+$, and subtraction $-$, if $a - b < c$, then $a < b + c$.
lt_add_of_tsub_lt_right theorem
(h : a - c < b) : a < b + c
Full source 
theorem lt_add_of_tsub_lt_right (h : a - c < b) : a < b + c :=
  Contravariant.AddLECancellable.lt_add_of_tsub_lt_right h
Strict Inequality from Truncated Subtraction: $a - c < b \Rightarrow a < b + c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, and subtraction $-$, if $a - c < b$, then $a < b + c$.
lt_tsub_of_add_lt_left theorem
: a + c < b → c < b - a
Full source 
/-- This lemma (and some of its corollaries) also holds for `ENNReal`, but this proof doesn't work
for it. Maybe we should add this lemma as field to `OrderedSub`? -/
theorem lt_tsub_of_add_lt_left : a + c < b → c < b - a :=
  Contravariant.AddLECancellable.lt_tsub_of_add_lt_left
Strict Subtraction Inequality Under Left Addition: $a + c < b \Rightarrow c < b - a$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, and subtraction $-$, if $a + c < b$, then $c < b - a$.
lt_tsub_of_add_lt_right theorem
: a + c < b → a < b - c
Full source 
theorem lt_tsub_of_add_lt_right : a + c < b → a < b - c :=
  Contravariant.AddLECancellable.lt_tsub_of_add_lt_right
Strict Subtraction Inequality: $a + c < b \Rightarrow a < b - c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, and subtraction $-$, if $a + c < b$, then $a < b - c$.
add_tsub_add_eq_tsub_right theorem
(a c b : α) : a + c - (b + c) = a - b
Full source 
theorem add_tsub_add_eq_tsub_right (a c b : α) : a + c - (b + c) = a - b := by
  refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)
  apply le_of_add_le_add_right
  rw [add_assoc]
  exact le_tsub_add
Right Cancellation Identity for Ordered Subtraction: $(a + c) - (b + c) = a - b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the equality $(a + c) - (b + c) = a - b$ holds.
add_tsub_add_eq_tsub_left theorem
(a b c : α) : a + b - (a + c) = b - c
Full source 
theorem add_tsub_add_eq_tsub_left (a b c : α) : a + b - (a + c) = b - c := by
  rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]
Left Cancellation Identity for Ordered Subtraction: $(a + b) - (a + c) = b - c$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the equality $(a + b) - (a + c) = b - c$ holds.
lt_of_tsub_lt_tsub_right theorem
(h : a - c < b - c) : a < b
Full source 
/-- See `lt_of_tsub_lt_tsub_right_of_le` for a weaker statement in a partial order. -/
theorem lt_of_tsub_lt_tsub_right (h : a - c < b - c) : a < b :=
  lt_imp_lt_of_le_imp_le (fun h => tsub_le_tsub_right h c) h
Strict Inequality from Subtraction: $a - c < b - c \Rightarrow a < b$
Informal description
For any elements $a, b, c$ in a linearly ordered type $\alpha$ with subtraction and addition satisfying the `OrderedSub` property, if $a - c < b - c$, then $a < b$.
lt_tsub_iff_right theorem
: a < b - c ↔ a + c < b
Full source 
/-- See `lt_tsub_iff_right_of_le` for a weaker statement in a partial order. -/
theorem lt_tsub_iff_right : a < b - c ↔ a + c < b :=
  lt_iff_lt_of_le_iff_le tsub_le_iff_right
Strict Inequality Characterization for Ordered Subtraction: $a < b - c \leftrightarrow a + c < b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a linear order $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the strict inequality $a < b - c$ holds if and only if $a + c < b$.
lt_tsub_iff_left theorem
: a < b - c ↔ c + a < b
Full source 
/-- See `lt_tsub_iff_left_of_le` for a weaker statement in a partial order. -/
theorem lt_tsub_iff_left : a < b - c ↔ c + a < b :=
  lt_iff_lt_of_le_iff_le tsub_le_iff_left
Left Strict Inequality Characterization for Ordered Subtraction: $a < b - c \leftrightarrow c + a < b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a preorder $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a < b - c$ holds if and only if $c + a < b$.
lt_tsub_comm theorem
: a < b - c ↔ c < b - a
Full source 
theorem lt_tsub_comm : a < b - c ↔ c < b - a :=
  lt_tsub_iff_left.trans lt_tsub_iff_right.symm
Commutative Characterization of Strict Inequalities in Ordered Subtraction: $a < b - c \leftrightarrow c < b - a$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a linear order $\leq$, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, the inequality $a < b - c$ holds if and only if $c < b - a$.
lt_of_tsub_lt_tsub_left theorem
(h : a - b < a - c) : c < b
Full source 
/-- See `lt_of_tsub_lt_tsub_left_of_le` for a weaker statement in a partial order. -/
theorem lt_of_tsub_lt_tsub_left (h : a - b < a - c) : c < b :=
  lt_imp_lt_of_le_imp_le (fun h => tsub_le_tsub_left h a) h
Strict Inequality Reversal via Subtraction: $a - b < a - c \Rightarrow c < b$
Informal description
For any elements $a, b, c$ in a type $\alpha$ equipped with a linear order, addition $+$, subtraction $-$, and satisfying the `OrderedSub` property, if $a - b < a - c$, then $c < b$.
tsub_zero theorem
(a : α) : a - 0 = a
Full source 
@[simp]
theorem tsub_zero (a : α) : a - 0 = a :=
  AddLECancellable.tsub_eq_of_eq_add addLECancellable_zero (add_zero _).symm
Subtraction of Zero: $a - 0 = a$
Informal description
For any element $a$ in a type $\alpha$ equipped with a subtraction operation and satisfying the `OrderedSub` property, subtracting zero from $a$ leaves it unchanged, i.e., $a - 0 = a$.