/-
Copyright (c) 2021 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn

! This file was ported from Lean 3 source module algebra.order.sub.defs
! leanprover-community/mathlib commit de29c328903507bb7aff506af9135f4bdaf1849c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.CovariantAndContravariant
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Order.Lattice

/-!
# 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 `CanonicallyOrderedAddMonoid` instance
(even though that is our main focus). Conversely, this means we can use
`CanonicallyOrderedAddMonoid` 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 `[ContravariantClass α α (+) (≤)]`. 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`
-/


variable {α: Type ?u.29977
α β: Type ?u.7101
β : Type _: Type (?u.5+1)
Type _}

/-- `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 u_1) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub (α: Type ?u.14
α : Type _: Type (?u.14+1)
Type _) [LE: Type ?u.17 → Type ?u.17
LE α: Type ?u.14
α] [Add: Type ?u.20 → Type ?u.20
Add α: Type ?u.14
α] [Sub: Type ?u.23 → Type ?u.23
Sub α: Type ?u.14
α] : Prop: Type
Prop where
  /-- `a - b` provides a lower bound on `c` such that `a ≤ c + b`. -/
  tsub_le_iff_right: ∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [self : OrderedSub α] (a b c : α),
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right : ∀ a: α
a b: α
b c: α
c : α: Type ?u.14
α, a: α
a - b: α
b ≤ c: α
c ↔ a: α
a ≤ c: α
c + b: α
b
#align has_ordered_sub OrderedSub: (α : Type u_1) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub

section Add

variable [Preorder: Type ?u.641 → Type ?u.641
Preorder α: Type ?u.176
α] [Add: Type ?u.644 → Type ?u.644
Add α: Type ?u.176
α] [Sub: Type ?u.188 → Type ?u.188
Sub α: Type ?u.128
α] [OrderedSub: (α : Type ?u.415) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub α: Type ?u.176
α] {a: α
a b: α
b c: α
c d: α
d : α: Type ?u.128
α}

@[simp]
theorem tsub_le_iff_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right : a: α
a - b: α
b ≤ c: α
c ↔ a: α
a ≤ c: α
c + b: α
b :=
  OrderedSub.tsub_le_iff_right: ∀ {α : Type ?u.317} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [self : OrderedSub α] (a b c : α),
  a - b ≤ c ↔ a ≤ c + b
OrderedSub.tsub_le_iff_right a: α
a b: α
b c: α
c
#align tsub_le_iff_right tsub_le_iff_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right

/-- See `add_tsub_cancel_right` for the equality if `ContravariantClass α α (+) (≤)`. -/
theorem add_tsub_le_right: a + b - b ≤ a
add_tsub_le_right : a: α
a + b: α
b - b: α
b ≤ a: α
a :=
  tsub_le_iff_right: ∀ {α : Type ?u.538} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr le_rfl: ∀ {α : Type ?u.589} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align add_tsub_le_right add_tsub_le_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}, a + b - b ≤ a
add_tsub_le_right

theorem le_tsub_add: b ≤ b - a + a
le_tsub_add : b: α
b ≤ b: α
b - a: α
a + a: α
a :=
  tsub_le_iff_right: ∀ {α : Type ?u.773} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp le_rfl: ∀ {α : Type ?u.824} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align le_tsub_add le_tsub_add: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}, b ≤ b - a + a
le_tsub_add

end Add

/-! ### Preorder -/


section OrderedAddCommSemigroup

section Preorder

variable [Preorder: Type ?u.9488 → Type ?u.9488
Preorder α: Type ?u.12332
α]

section AddCommSemigroup

variable [AddCommSemigroup: Type ?u.4901 → Type ?u.4901
AddCommSemigroup α: Type ?u.4451
α] [Sub: Type ?u.8417 → Type ?u.8417
Sub α: Type ?u.1813
α] [OrderedSub: (α : Type ?u.9497) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub α: Type ?u.2409
α] {a: α
a b: α
b c: α
c d: α
d : α: Type ?u.879
α}

theorem tsub_le_iff_left: a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left : a: α
a - b: α
b ≤ c: α
c ↔ a: α
a ≤ b: α
b + c: α
c := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.1063

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a ≤ b + crw [α: Type u_1

β: Type ?u.1063

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a ≤ b + ctsub_le_iff_right: ∀ {α : Type ?u.1565} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right,α: Type u_1

β: Type ?u.1063

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ c + b ↔ a ≤ b + c α: Type u_1

β: Type ?u.1063

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a ≤ b + cadd_comm: ∀ {G : Type ?u.1771} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_commα: Type u_1

β: Type ?u.1063

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ b + c ↔ a ≤ b + c]
Goals accomplished! 🐙
#align tsub_le_iff_left tsub_le_iff_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left

theorem le_add_tsub: a ≤ b + (a - b)
le_add_tsub : a: α
a ≤ b: α
b + (a: α
a - b: α
b) :=
  tsub_le_iff_left: ∀ {α : Type ?u.2314} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp le_rfl: ∀ {α : Type ?u.2367} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align le_add_tsub le_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a ≤ b + (a - b)
le_add_tsub

/-- See `add_tsub_cancel_left` for the equality if `ContravariantClass α α (+) (≤)`. -/
theorem add_tsub_le_left: a + b - a ≤ b
add_tsub_le_left : a: α
a + b: α
b - a: α
a ≤ b: α
b :=
  tsub_le_iff_left: ∀ {α : Type ?u.2910} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr le_rfl: ∀ {α : Type ?u.2960} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align add_tsub_le_left add_tsub_le_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a + b - a ≤ b
add_tsub_le_left

theorem tsub_le_tsub_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a ≤ b → ∀ (c : α), a - c ≤ b - c
tsub_le_tsub_right (h: a ≤ b
h : a: α
a ≤ b: α
b) (c: α
c : α: Type ?u.3005
α) : a: α
a - c: α
c ≤ b: α
b - c: α
c :=
  tsub_le_iff_left: ∀ {α : Type ?u.3270} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr <| h: a ≤ b
h.trans: ∀ {α : Type ?u.3320} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans le_add_tsub: ∀ {α : Type ?u.3333} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub
#align tsub_le_tsub_right tsub_le_tsub_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a ≤ b → ∀ (c : α), a - c ≤ b - c
tsub_le_tsub_right

theorem tsub_le_iff_tsub_le: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a - c ≤ b
tsub_le_iff_tsub_le : a: α
a - b: α
b ≤ c: α
c ↔ a: α
a - c: α
c ≤ b: α
b := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.3403

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a - c ≤ brw [α: Type u_1

β: Type ?u.3403

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a - c ≤ btsub_le_iff_left: ∀ {α : Type ?u.3658} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.3403

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ b + c ↔ a - c ≤ b α: Type u_1

β: Type ?u.3403

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ c ↔ a - c ≤ btsub_le_iff_right: ∀ {α : Type ?u.3728} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_rightα: Type u_1

β: Type ?u.3403

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ b + c ↔ a ≤ b + c]
Goals accomplished! 🐙
#align tsub_le_iff_tsub_le tsub_le_iff_tsub_le: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a - c ≤ b
tsub_le_iff_tsub_le

/-- See `tsub_tsub_cancel_of_le` for the equality. -/
theorem tsub_tsub_le: b - (b - a) ≤ a
tsub_tsub_le : b: α
b - (b: α
b - a: α
a) ≤ a: α
a :=
  tsub_le_iff_right: ∀ {α : Type ?u.4204} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr le_add_tsub: ∀ {α : Type ?u.4255} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub
#align tsub_tsub_le tsub_tsub_le: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  b - (b - a) ≤ a
tsub_tsub_le

section Cov

variable [CovariantClass: (M : Type ?u.9664) → (N : Type ?u.9663) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass α: Type ?u.4892
α α: Type ?u.4451
α (· + ·): α → α → α
(· + ·) (· ≤ ·): α → α → Prop
(· ≤ ·)]

theorem tsub_le_tsub_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → ∀ (c : α), c - b ≤ c - a
tsub_le_tsub_left (h: a ≤ b
h : a: α
a ≤ b: α
b) (c: α
c : α: Type ?u.4892
α) : c: α
c - b: α
b ≤ c: α
c - a: α
a :=
  tsub_le_iff_left: ∀ {α : Type ?u.5417} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr <| le_add_tsub: ∀ {α : Type ?u.5467} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub.trans: ∀ {α : Type ?u.5495} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| add_le_add_right: ∀ {α : Type ?u.5540} [inst : Add α] [inst_1 : LE α]
  [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α},
  b ≤ c → ∀ (a : α), b + a ≤ c + a
add_le_add_right h: a ≤ b
h _: ?m.5541
_
#align tsub_le_tsub_left tsub_le_tsub_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → ∀ (c : α), c - b ≤ c - a
tsub_le_tsub_left

theorem tsub_le_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → c ≤ d → a - d ≤ b - c
tsub_le_tsub (hab: a ≤ b
hab : a: α
a ≤ b: α
b) (hcd: c ≤ d
hcd : c: α
c ≤ d: α
d) : a: α
a - d: α
d ≤ b: α
b - c: α
c :=
  (tsub_le_tsub_right: ∀ {α : Type ?u.6333} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b → ∀ (c : α), a - c ≤ b - c
tsub_le_tsub_right hab: a ≤ b
hab _: ?m.6334
_).trans: ∀ {α : Type ?u.6367} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| tsub_le_tsub_left: ∀ {α : Type ?u.6390} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → ∀ (c : α), c - b ≤ c - a
tsub_le_tsub_left hcd: c ≤ d
hcd _: ?m.6391
_
#align tsub_le_tsub tsub_le_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → c ≤ d → a - d ≤ b - c
tsub_le_tsub

theorem antitone_const_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], Antitone fun x => c - x
antitone_const_tsub : Antitone: {α : Type ?u.6880} → {β : Type ?u.6879} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone fun x: ?m.6904
x => c: α
c - x: ?m.6904
x := fun _: ?m.6951
_ _: ?m.6954
_ hxy: ?m.6957
hxy => tsub_le_tsub: ∀ {α : Type ?u.6959} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → c ≤ d → a - d ≤ b - c
tsub_le_tsub rfl: ∀ {α : Sort ?u.7017} {a : α}, a = a
rfl.le: ∀ {α : Type ?u.7020} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le hxy: ?m.6957
hxy
#align antitone_const_tsub antitone_const_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], Antitone fun x => c - x
antitone_const_tsub

/-- See `add_tsub_assoc_of_le` for the equality. -/
theorem add_tsub_le_assoc: a + b - c ≤ a + (b - c)
add_tsub_le_assoc : a: α
a + b: α
b - c: α
c ≤ a: α
a + (b: α
b - c: α
c) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a + (b - c)rw [α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a + (b - c)tsub_le_iff_left: ∀ {α : Type ?u.8003} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ c + (a + (b - c)) α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a + (b - c)add_left_comm: ∀ {G : Type ?u.8073} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)
add_left_commα: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))]α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))
  α: Type u_1

β: Type ?u.7101

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a + (b - c)exact add_le_add_left: ∀ {α : Type ?u.8145} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left le_add_tsub: ∀ {α : Type ?u.8152} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub a: α
a
Goals accomplished! 🐙
#align add_tsub_le_assoc add_tsub_le_assoc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a + (b - c)
add_tsub_le_assoc

/-- See `tsub_add_eq_add_tsub` for the equality. -/
theorem add_tsub_le_tsub_add: a + b - c ≤ a - c + b
add_tsub_le_tsub_add : a: α
a + b: α
b - c: α
c ≤ a: α
a - c: α
c + b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a - c + brw [α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a - c + badd_comm: ∀ {G : Type ?u.9310} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a - c ≤ a - c + b α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a - c + badd_comm: ∀ {G : Type ?u.9335} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm _: ?m.9336
_ b: α
bα: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a - c ≤ b + (a - c)]α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a - c ≤ b + (a - c)
  α: Type u_1

β: Type ?u.8408

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - c ≤ a - c + bexact add_tsub_le_assoc: ∀ {α : Type ?u.9390} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a + (b - c)
add_tsub_le_assoc
Goals accomplished! 🐙
#align add_tsub_le_tsub_add add_tsub_le_tsub_add: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a - c + b
add_tsub_le_tsub_add

theorem add_le_add_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ a + c + (b - c)
add_le_add_add_tsub : a: α
a + b: α
b ≤ a: α
a + c: α
c + (b: α
b - c: α
c) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.9485

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + c + (b - c)rw [α: Type u_1

β: Type ?u.9485

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + c + (b - c)add_assoc: ∀ {G : Type ?u.10486} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assocα: Type u_1

β: Type ?u.9485

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))]α: Type u_1

β: Type ?u.9485

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))
  α: Type u_1

β: Type ?u.9485

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + c + (b - c)exact add_le_add_left: ∀ {α : Type ?u.10890} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left le_add_tsub: ∀ {α : Type ?u.10897} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub a: α
a
Goals accomplished! 🐙
#align add_le_add_add_tsub add_le_add_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ a + c + (b - c)
add_le_add_add_tsub

theorem le_tsub_add_add: a + b ≤ a - c + (b + c)
le_tsub_add_add : a: α
a + b: α
b ≤ a: α
a - c: α
c + (b: α
b + c: α
c) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a - c + (b + c)rw [α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a - c + (b + c)add_comm: ∀ {G : Type ?u.12137} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm a: α
a,α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a ≤ a - c + (b + c) α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a - c + (b + c)add_comm: ∀ {G : Type ?u.12154} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm (a: α
a - c: α
c)α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a ≤ b + c + (a - c)]α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b + a ≤ b + c + (a - c)
  α: Type u_1

β: Type ?u.11136

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a - c + (b + c)exact add_le_add_add_tsub: ∀ {α : Type ?u.12239} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ a + c + (b - c)
add_le_add_add_tsub
Goals accomplished! 🐙
#align le_tsub_add_add le_tsub_add_add: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ a - c + (b + c)
le_tsub_add_add

theorem tsub_le_tsub_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a - c ≤ a - b + (b - c)
tsub_le_tsub_add_tsub : a: α
a - c: α
c ≤ a: α
a - b: α
b + (b: α
b - c: α
c) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a - c ≤ a - b + (b - c)rw [α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a - c ≤ a - b + (b - c)tsub_le_iff_left: ∀ {α : Type ?u.13138} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a ≤ c + (a - b + (b - c)) α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a - c ≤ a - b + (b - c)← add_assoc: ∀ {G : Type ?u.13208} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc,α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a ≤ c + (a - b) + (b - c) α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a - c ≤ a - b + (b - c)add_right_comm: ∀ {G : Type ?u.13564} [inst : AddCommSemigroup G] (a b c : G), a + b + c = a + c + b
add_right_commα: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a ≤ c + (b - c) + (a - b)]α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a ≤ c + (b - c) + (a - b)
  α: Type u_1

β: Type ?u.12335

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a - c ≤ a - b + (b - c)exact le_add_tsub: ∀ {α : Type ?u.13616} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub.trans: ∀ {α : Type ?u.13644} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans (add_le_add_right: ∀ {α : Type ?u.13693} [inst : Add α] [inst_1 : LE α]
  [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α},
  b ≤ c → ∀ (a : α), b + a ≤ c + a
add_le_add_right le_add_tsub: ∀ {α : Type ?u.13700} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub _: ?m.13694
_)
Goals accomplished! 🐙
#align tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a - c ≤ a - b + (b - c)
tsub_le_tsub_add_tsub

theorem tsub_tsub_tsub_le_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], c - a - (c - b) ≤ b - a
tsub_tsub_tsub_le_tsub : c: α
c - a: α
a - (c: α
c - b: α
b) ≤ b: α
b - a: α
a := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a - (c - b) ≤ b - arw [α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a - (c - b) ≤ b - atsub_le_iff_left: ∀ {α : Type ?u.14549} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a ≤ c - b + (b - a) α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a - (c - b) ≤ b - atsub_le_iff_left: ∀ {α : Type ?u.14619} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c ≤ a + (c - b + (b - a)) α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a - (c - b) ≤ b - aadd_left_comm: ∀ {G : Type ?u.14664} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)
add_left_commα: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c ≤ c - b + (a + (b - a))]α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c ≤ c - b + (a + (b - a))
  α: Type u_1

β: Type ?u.13993

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

c - a - (c - b) ≤ b - aexact le_tsub_add: ∀ {α : Type ?u.14724} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  b ≤ b - a + a
le_tsub_add.trans: ∀ {α : Type ?u.14753} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans (add_le_add_left: ∀ {α : Type ?u.14802} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left le_add_tsub: ∀ {α : Type ?u.14809} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub _: ?m.14803
_)
Goals accomplished! 🐙
#align tsub_tsub_tsub_le_tsub tsub_tsub_tsub_le_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], c - a - (c - b) ≤ b - a
tsub_tsub_tsub_le_tsub

theorem tsub_tsub_le_tsub_add: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a - (b - c) ≤ a - b + c
tsub_tsub_le_tsub_add {a: α
a b: α
b c: α
c : α: Type ?u.15083
α} : a: α
a - (b: α
b - c: α
c) ≤ a: α
a - b: α
b + c: α
c :=
  tsub_le_iff_right: ∀ {α : Type ?u.15900} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <|
    calc
      a: α
a ≤ a: α
a - b: α
b + b: α
b := le_tsub_add: ∀ {α : Type ?u.16268} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  b ≤ b - a + a
le_tsub_add
      _: ?m✝
_ ≤ a: α
a - b: α
b + (c: α
c + (b: α
b - c: α
c)) := add_le_add_left: ∀ {α : Type ?u.16710} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left le_add_tsub: ∀ {α : Type ?u.16717} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub _: ?m.16711
_
      _: ?m✝
_ = a: α
a - b: α
b + c: α
c + (b: α
b - c: α
c) := (add_assoc: ∀ {G : Type ?u.17180} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc _: ?m.17181
_ _: ?m.17181
_ _: ?m.17181
_).symm: ∀ {α : Sort ?u.17308} {a b : α}, a = b → b = a
symm
#align tsub_tsub_le_tsub_add tsub_tsub_le_tsub_add: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a - (b - c) ≤ a - b + c
tsub_tsub_le_tsub_add

/-- See `tsub_add_tsub_comm` for the equality. -/
theorem add_tsub_add_le_tsub_add_tsub: a + b - (c + d) ≤ a - c + (b - d)
add_tsub_add_le_tsub_add_tsub : a: α
a + b: α
b - (c: α
c + d: α
d) ≤ a: α
a - c: α
c + (b: α
b - d: α
d) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)rw [α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)add_comm: ∀ {G : Type ?u.18526} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm c: α
c,α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (d + c) ≤ a - c + (b - d) α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)tsub_le_iff_left: ∀ {α : Type ?u.18549} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ d + c + (a - c + (b - d)) α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)add_assoc: ∀ {G : Type ?u.18616} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc,α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ d + (c + (a - c + (b - d))) α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)← tsub_le_iff_left: ∀ {α : Type ?u.18972} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - d ≤ c + (a - c + (b - d)) α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)← tsub_le_iff_left: ∀ {α : Type ?u.19017} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_leftα: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - d - c ≤ a - c + (b - d)]α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - d - c ≤ a - c + (b - d)
  α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)refine' (tsub_le_tsub_right: ∀ {α : Type ?u.19103} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b → ∀ (c : α), a - c ≤ b - c
tsub_le_tsub_right add_tsub_le_assoc: ∀ {α : Type ?u.19111} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a + (b - c)
add_tsub_le_assoc c: α
c).trans: ∀ {α : Type ?u.19208} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans _: ?m.19219 ≤ ?m.19220
_α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + (b - d) - c ≤ a - c + (b - d)
  α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)rw [α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + (b - d) - c ≤ a - c + (b - d)add_comm: ∀ {G : Type ?u.19247} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm a: α
a,α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b - d + a - c ≤ a - c + (b - d) α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + (b - d) - c ≤ a - c + (b - d)add_comm: ∀ {G : Type ?u.19255} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm (a: α
a - c: α
c)α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b - d + a - c ≤ b - d + (a - c)]α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

b - d + a - c ≤ b - d + (a - c)
  α: Type u_1

β: Type ?u.17481

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (c + d) ≤ a - c + (b - d)exact add_tsub_le_assoc: ∀ {α : Type ?u.19333} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a + (b - c)
add_tsub_le_assoc
Goals accomplished! 🐙
#align add_tsub_add_le_tsub_add_tsub add_tsub_add_le_tsub_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
  a + b - (c + d) ≤ a - c + (b - d)
add_tsub_add_le_tsub_add_tsub

/-- See `add_tsub_add_eq_tsub_left` for the equality. -/
theorem add_tsub_add_le_tsub_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - (a + c) ≤ b - c
add_tsub_add_le_tsub_left : a: α
a + b: α
b - (a: α
a + c: α
c) ≤ b: α
b - c: α
c := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (a + c) ≤ b - crw [α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (a + c) ≤ b - ctsub_le_iff_left: ∀ {α : Type ?u.20299} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + c + (b - c) α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (a + c) ≤ b - cadd_assoc: ∀ {G : Type ?u.20369} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assocα: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))]α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b ≤ a + (c + (b - c))
  α: Type u_1

β: Type ?u.19397

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + b - (a + c) ≤ b - cexact add_le_add_left: ∀ {α : Type ?u.20772} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left le_add_tsub: ∀ {α : Type ?u.20779} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub _: ?m.20773
_
Goals accomplished! 🐙
#align add_tsub_add_le_tsub_left add_tsub_add_le_tsub_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - (a + c) ≤ b - c
add_tsub_add_le_tsub_left

/-- See `add_tsub_add_eq_tsub_right` for the equality. -/
theorem add_tsub_add_le_tsub_right: a + c - (b + c) ≤ a - b
add_tsub_add_le_tsub_right : a: α
a + c: α
c - (b: α
b + c: α
c) ≤ a: α
a - b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c - (b + c) ≤ a - brw [α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c - (b + c) ≤ a - btsub_le_iff_left: ∀ {α : Type ?u.21931} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c ≤ b + c + (a - b) α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c - (b + c) ≤ a - badd_right_comm: ∀ {G : Type ?u.22001} [inst : AddCommSemigroup G] (a b c : G), a + b + c = a + c + b
add_right_commα: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c ≤ b + (a - b) + c]α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c ≤ b + (a - b) + c
  α: Type u_1

β: Type ?u.21029

inst✝⁴: Preorder α

inst✝³: AddCommSemigroup α

inst✝²: Sub α

inst✝¹: OrderedSub α

a, b, c, d: α

inst✝: CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

a + c - (b + c) ≤ a - bexact add_le_add_right: ∀ {α : Type ?u.22073} [inst : Add α] [inst_1 : LE α]
  [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α},
  b ≤ c → ∀ (a : α), b + a ≤ c + a
add_le_add_right le_add_tsub: ∀ {α : Type ?u.22080} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub c: α
c
Goals accomplished! 🐙
#align add_tsub_add_le_tsub_right add_tsub_add_le_tsub_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + c - (b + c) ≤ a - b
add_tsub_add_le_tsub_right

end Cov

/-! #### Lemmas that assume that an element is `AddLECancellable` -/


namespace AddLECancellable

protected theorem le_add_tsub_swap: AddLECancellable b → a ≤ b + a - b
le_add_tsub_swap (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.22558} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) : a: α
a ≤ b: α
b + a: α
a - b: α
b :=
  hb: AddLECancellable b
hb le_add_tsub: ∀ {α : Type ?u.23009} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub
#align add_le_cancellable.le_add_tsub_swap AddLECancellable.le_add_tsub_swap: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  AddLECancellable b → a ≤ b + a - b
AddLECancellable.le_add_tsub_swap

protected theorem le_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  AddLECancellable b → a ≤ a + b - b
le_add_tsub (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.23264} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) : a: α
a ≤ a: α
a + b: α
b - b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.23086

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a ≤ a + b - brw [α: Type u_1

β: Type ?u.23086

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a ≤ a + b - badd_comm: ∀ {G : Type ?u.23711} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_commα: Type u_1

β: Type ?u.23086

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a ≤ b + a - b]α: Type u_1

β: Type ?u.23086

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a ≤ b + a - b
  α: Type u_1

β: Type ?u.23086

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a ≤ a + b - bexact hb: AddLECancellable b
hb.le_add_tsub_swap: ∀ {α : Type ?u.23771} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a ≤ b + a - b
le_add_tsub_swap
Goals accomplished! 🐙
#align add_le_cancellable.le_add_tsub AddLECancellable.le_add_tsub: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  AddLECancellable b → a ≤ a + b - b
AddLECancellable.le_add_tsub

protected theorem le_tsub_of_add_le_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  AddLECancellable a → a + b ≤ c → b ≤ c - a
le_tsub_of_add_le_left (ha: AddLECancellable a
ha : AddLECancellable: {α : Type ?u.23996} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable a: α
a) (h: a + b ≤ c
h : a: α
a + b: α
b ≤ c: α
c) : b: α
b ≤ c: α
c - a: α
a :=
  ha: AddLECancellable a
ha <| h: a + b ≤ c
h.trans: ∀ {α : Type ?u.24454} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans le_add_tsub: ∀ {α : Type ?u.24471} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, a ≤ b + (a - b)
le_add_tsub
#align add_le_cancellable.le_tsub_of_add_le_left AddLECancellable.le_tsub_of_add_le_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  AddLECancellable a → a + b ≤ c → b ≤ c - a
AddLECancellable.le_tsub_of_add_le_left

protected theorem le_tsub_of_add_le_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  AddLECancellable b → a + b ≤ c → a ≤ c - b
le_tsub_of_add_le_right (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.24724} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) (h: a + b ≤ c
h : a: α
a + b: α
b ≤ c: α
c) : a: α
a ≤ c: α
c - b: α
b :=
  hb: AddLECancellable b
hb.le_tsub_of_add_le_left: ∀ {α : Type ?u.25176} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable a → a + b ≤ c → b ≤ c - a
le_tsub_of_add_le_left <| by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.24546

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a + b ≤ c

b + a ≤ crwa [α: Type u_1

β: Type ?u.24546

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a + b ≤ c

b + a ≤ cadd_comm: ∀ {G : Type ?u.25232} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_commα: Type u_1

β: Type ?u.24546

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a + b ≤ c

a + b ≤ c]α: Type u_1

β: Type ?u.24546

inst✝³: Preorder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a + b ≤ c

a + b ≤ c
#align add_le_cancellable.le_tsub_of_add_le_right AddLECancellable.le_tsub_of_add_le_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  AddLECancellable b → a + b ≤ c → a ≤ c - b
AddLECancellable.le_tsub_of_add_le_right

end AddLECancellable

/-! ### Lemmas where addition is order-reflecting -/


section Contra

variable [ContravariantClass: (M : Type ?u.25925) → (N : Type ?u.25924) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass α: Type ?u.25743
α α: Type ?u.25302
α (· + ·): α → α → α
(· + ·) (· ≤ ·): α → α → Prop
(· ≤ ·)]

theorem le_add_tsub_swap: a ≤ b + a - b
le_add_tsub_swap : a: α
a ≤ b: α
b + a: α
a - b: α
b :=
  Contravariant.AddLECancellable: ∀ {α : Type ?u.26504} [inst : Add α] [inst_1 : LE α]
  [inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, AddLECancellable a
Contravariant.AddLECancellable.le_add_tsub_swap: ∀ {α : Type ?u.26537} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a ≤ b + a - b
le_add_tsub_swap
#align le_add_tsub_swap le_add_tsub_swap: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b + a - b
le_add_tsub_swap

theorem le_add_tsub': ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ a + b - b
le_add_tsub' : a: α
a ≤ a: α
a + b: α
b - b: α
b :=
  Contravariant.AddLECancellable: ∀ {α : Type ?u.27555} [inst : Add α] [inst_1 : LE α]
  [inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, AddLECancellable a
Contravariant.AddLECancellable.le_add_tsub: ∀ {α : Type ?u.27588} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a ≤ a + b - b
le_add_tsub
#align le_add_tsub' le_add_tsub': ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ a + b - b
le_add_tsub'

theorem le_tsub_of_add_le_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ c → b ≤ c - a
le_tsub_of_add_le_left (h: a + b ≤ c
h : a: α
a + b: α
b ≤ c: α
c) : b: α
b ≤ c: α
c - a: α
a :=
  Contravariant.AddLECancellable: ∀ {α : Type ?u.28613} [inst : Add α] [inst_1 : LE α]
  [inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, AddLECancellable a
Contravariant.AddLECancellable.le_tsub_of_add_le_left: ∀ {α : Type ?u.28646} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable a → a + b ≤ c → b ≤ c - a
le_tsub_of_add_le_left h: a + b ≤ c
h
#align le_tsub_of_add_le_left le_tsub_of_add_le_left: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ c → b ≤ c - a
le_tsub_of_add_le_left

theorem le_tsub_of_add_le_right: a + b ≤ c → a ≤ c - b
le_tsub_of_add_le_right (h: a + b ≤ c
h : a: α
a + b: α
b ≤ c: α
c) : a: α
a ≤ c: α
c - b: α
b :=
  Contravariant.AddLECancellable: ∀ {α : Type ?u.29679} [inst : Add α] [inst_1 : LE α]
  [inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, AddLECancellable a
Contravariant.AddLECancellable.le_tsub_of_add_le_right: ∀ {α : Type ?u.29712} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a + b ≤ c → a ≤ c - b
le_tsub_of_add_le_right h: a + b ≤ c
h
#align le_tsub_of_add_le_right le_tsub_of_add_le_right: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α}
  [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ c → a ≤ c - b
le_tsub_of_add_le_right

end Contra

end AddCommSemigroup

variable [AddCommMonoid: Type ?u.30130 → Type ?u.30130
AddCommMonoid α: Type ?u.30121
α] [Sub: Type ?u.29989 → Type ?u.29989
Sub α: Type ?u.30121
α] [OrderedSub: (α : Type ?u.29992) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub α: Type ?u.30121
α] {a: α
a b: α
b c: α
c d: α
d : α: Type ?u.29977
α}

theorem tsub_nonpos: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a - b ≤ 0 ↔ a ≤ b
tsub_nonpos : a: α
a - b: α
b ≤ 0: ?m.30270
0 ↔ a: α
a ≤ b: α
b := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.30124

inst✝³: Preorder α

inst✝²: AddCommMonoid α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ 0 ↔ a ≤ brw [α: Type u_1

β: Type ?u.30124

inst✝³: Preorder α

inst✝²: AddCommMonoid α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ 0 ↔ a ≤ btsub_le_iff_left: ∀ {α : Type ?u.30455} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.30124

inst✝³: Preorder α

inst✝²: AddCommMonoid α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ b + 0 ↔ a ≤ b α: Type u_1

β: Type ?u.30124

inst✝³: Preorder α

inst✝²: AddCommMonoid α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b ≤ 0 ↔ a ≤ badd_zero: ∀ {M : Type ?u.30551} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zeroα: Type u_1

β: Type ?u.30124

inst✝³: Preorder α

inst✝²: AddCommMonoid α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a ≤ b ↔ a ≤ b]
Goals accomplished! 🐙
#align tsub_nonpos tsub_nonpos: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a - b ≤ 0 ↔ a ≤ b
tsub_nonpos

alias tsub_nonpos: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a - b ≤ 0 ↔ a ≤ b
tsub_nonpos ↔ _ tsub_nonpos_of_le: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a ≤ b → a - b ≤ 0
tsub_nonpos_of_le
#align tsub_nonpos_of_le tsub_nonpos_of_le: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
  a ≤ b → a - b ≤ 0
tsub_nonpos_of_le

end Preorder

/-! ### Partial order -/


variable [PartialOrder: Type ?u.36808 → Type ?u.36808
PartialOrder α: Type ?u.47125
α] [AddCommSemigroup: Type ?u.38304 → Type ?u.38304
AddCommSemigroup α: Type ?u.40618
α] [Sub: Type ?u.41602 → Type ?u.41602
Sub α: Type ?u.30853
α] [OrderedSub: (α : Type ?u.39416) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub α: Type ?u.31041
α] {a: α
a b: α
b c: α
c d: α
d : α: Type ?u.36059
α}

theorem tsub_tsub: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (b a c : α), b - a - c = b - (a + c)
tsub_tsub (b: α
b a: α
a c: α
c : α: Type ?u.31041
α) : b: α
b - a: α
a - c: α
c = b: α
b - (a: α
a + c: α
c) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

b - a - c = b - (a + c)apply le_antisymm: ∀ {α : Type ?u.31593} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymmα: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)
α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - c
  α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

b - a - c = b - (a + c)·α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)
α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - crw [α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)tsub_le_iff_left: ∀ {α : Type ?u.31614} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a ≤ c + (b - (a + c)) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)tsub_le_iff_left: ∀ {α : Type ?u.31699} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab ≤ a + (c + (b - (a + c))) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)← add_assoc: ∀ {G : Type ?u.31752} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab ≤ a + c + (b - (a + c)) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - (a + c)← tsub_le_iff_left: ∀ {α : Type ?u.32108} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_leftα: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - (a + c)]
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

b - a - c = b - (a + c)·α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - c α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - crw [α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - ctsub_le_iff_left: ∀ {α : Type ?u.32176} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab ≤ a + c + (b - a - c) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - cadd_assoc: ∀ {G : Type ?u.32229} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab ≤ a + (c + (b - a - c)) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - c← tsub_le_iff_left: ∀ {α : Type ?u.32455} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_left,α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a ≤ c + (b - a - c) α: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - (a + c) ≤ b - a - c← tsub_le_iff_left: ∀ {α : Type ?u.32508} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, a - b ≤ c ↔ a ≤ b + c
tsub_le_iff_leftα: Type u_1

β: Type ?u.31044

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, b, a, c: α

ab - a - c ≤ b - a - c]
Goals accomplished! 🐙
#align tsub_tsub tsub_tsub: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (b a c : α), b - a - c = b - (a + c)
tsub_tsub

theorem tsub_add_eq_tsub_tsub: ∀ (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub (a: α
a b: α
b c: α
c : α: Type ?u.32593
α) : a: α
a - (b: α
b + c: α
c) = a: α
a - b: α
b - c: α
c :=
  (tsub_tsub: ∀ {α : Type ?u.33143} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (b a c : α), b - a - c = b - (a + c)
tsub_tsub _: ?m.33144
_ _: ?m.33144
_ _: ?m.33144
_).symm: ∀ {α : Sort ?u.33174} {a b : α}, a = b → b = a
symm
#align tsub_add_eq_tsub_tsub tsub_add_eq_tsub_tsub: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub

theorem tsub_add_eq_tsub_tsub_swap: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - c - b
tsub_add_eq_tsub_tsub_swap (a: α
a b: α
b c: α
c : α: Type ?u.33250
α) : a: α
a - (b: α
b + c: α
c) = a: α
a - c: α
c - b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.33253

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, a, b, c: α

a - (b + c) = a - c - brw [α: Type u_1

β: Type ?u.33253

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, a, b, c: α

a - (b + c) = a - c - badd_comm: ∀ {G : Type ?u.33802} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_commα: Type u_1

β: Type ?u.33253

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, a, b, c: α

a - (c + b) = a - c - b]α: Type u_1

β: Type ?u.33253

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, a, b, c: α

a - (c + b) = a - c - b
  α: Type u_1

β: Type ?u.33253

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a✝, b✝, c✝, d, a, b, c: α

a - (b + c) = a - c - bapply tsub_add_eq_tsub_tsub: ∀ {α : Type ?u.33847} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub
Goals accomplished! 🐙
#align tsub_add_eq_tsub_tsub_swap tsub_add_eq_tsub_tsub_swap: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - c - b
tsub_add_eq_tsub_tsub_swap

theorem tsub_right_comm: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  {a b c : α}, a - b - c = a - c - b
tsub_right_comm : a: α
a - b: α
b - c: α
c = a: α
a - c: α
c - b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.33907

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b - c = a - c - brw [α: Type u_1

β: Type ?u.33907

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b - c = a - c - b←tsub_add_eq_tsub_tsub: ∀ {α : Type ?u.34199} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub,α: Type u_1

β: Type ?u.33907

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - (b + c) = a - c - b α: Type u_1

β: Type ?u.33907

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - b - c = a - c - btsub_add_eq_tsub_tsub_swap: ∀ {α : Type ?u.34275} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - c - b
tsub_add_eq_tsub_tsub_swapα: Type u_1

β: Type ?u.33907

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

a - c - b = a - c - b]
Goals accomplished! 🐙
#align tsub_right_comm tsub_right_comm: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  {a b c : α}, a - b - c = a - c - b
tsub_right_comm

/-! ### Lemmas that assume that an element is `AddLECancellable`. -/


namespace AddLECancellable

protected theorem tsub_eq_of_eq_add: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
tsub_eq_of_eq_add (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.34538} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) (h: a = c + b
h : a: α
a = c: α
c + b: α
b) : a: α
a - b: α
b = c: α
c :=
  le_antisymm: ∀ {α : Type ?u.34993} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (tsub_le_iff_right: ∀ {α : Type ?u.35012} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr h: a = c + b
h.le: ∀ {α : Type ?u.35078} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le) <| by
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.34353

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = c + b

c ≤ a - brw [α: Type u_1

β: Type ?u.34353

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = c + b

c ≤ a - bh: a = c + b
hα: Type u_1

β: Type ?u.34353

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = c + b

c ≤ c + b - b]α: Type u_1

β: Type ?u.34353

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = c + b

c ≤ c + b - b
    α: Type u_1

β: Type ?u.34353

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = c + b

c ≤ a - bexact hb: AddLECancellable b
hb.le_add_tsub: ∀ {α : Type ?u.35300} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a ≤ a + b - b
le_add_tsub
Goals accomplished! 🐙
#align add_le_cancellable.tsub_eq_of_eq_add AddLECancellable.tsub_eq_of_eq_add: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
AddLECancellable.tsub_eq_of_eq_add

protected theorem eq_tsub_of_add_eq: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable c → a + c = b → a = b - c
eq_tsub_of_add_eq (hc: AddLECancellable c
hc : AddLECancellable: {α : Type ?u.35522} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable c: α
c) (h: a + c = b
h : a: α
a + c: α
c = b: α
b) : a: α
a = b: α
b - c: α
c :=
  (hc: AddLECancellable c
hc.tsub_eq_of_eq_add: ∀ {α : Type ?u.35977} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
tsub_eq_of_eq_add h: a + c = b
h.symm: ∀ {α : Sort ?u.36010} {a b : α}, a = b → b = a
symm).symm: ∀ {α : Sort ?u.36040} {a b : α}, a = b → b = a
symm
#align add_le_cancellable.eq_tsub_of_add_eq AddLECancellable.eq_tsub_of_add_eq: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable c → a + c = b → a = b - c
AddLECancellable.eq_tsub_of_add_eq

protected theorem tsub_eq_of_eq_add_rev: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = b + c → a - b = c
tsub_eq_of_eq_add_rev (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.36247} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) (h: a = b + c
h : a: α
a = b: α
b + c: α
c) : a: α
a - b: α
b = c: α
c :=
  hb: AddLECancellable b
hb.tsub_eq_of_eq_add: ∀ {α : Type ?u.36702} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
tsub_eq_of_eq_add <| by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.36062

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = b + c

a = c + brw [α: Type u_1

β: Type ?u.36062

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = b + c

a = c + badd_comm: ∀ {G : Type ?u.36759} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,α: Type u_1

β: Type ?u.36062

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = b + c

a = b + c α: Type u_1

β: Type ?u.36062

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = b + c

a = c + bh: a = b + c
hα: Type u_1

β: Type ?u.36062

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a = b + c

b + c = b + c]
Goals accomplished! 🐙
#align add_le_cancellable.tsub_eq_of_eq_add_rev AddLECancellable.tsub_eq_of_eq_add_rev: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = b + c → a - b = c
AddLECancellable.tsub_eq_of_eq_add_rev

@[simp]
protected theorem add_tsub_cancel_right: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a + b - b = a
add_tsub_cancel_right (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.36990} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) : a: α
a + b: α
b - b: α
b = a: α
a :=
  hb: AddLECancellable b
hb.tsub_eq_of_eq_add: ∀ {α : Type ?u.37440} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
tsub_eq_of_eq_add <| by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.36805

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a + b = a + brw [α: Type u_1

β: Type ?u.36805

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

a + b = a + badd_comm: ∀ {G : Type ?u.37497} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_commα: Type u_1

β: Type ?u.36805

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

b + a = b + a]
Goals accomplished! 🐙
#align add_le_cancellable.add_tsub_cancel_right AddLECancellable.add_tsub_cancel_right: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable b → a + b - b = a
AddLECancellable.add_tsub_cancel_right

@[simp]
protected theorem add_tsub_cancel_left: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable a → a + b - a = b
add_tsub_cancel_left (ha: AddLECancellable a
ha : AddLECancellable: {α : Type ?u.37750} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable a: α
a) : a: α
a + b: α
b - a: α
a = b: α
b :=
  ha: AddLECancellable a
ha.tsub_eq_of_eq_add: ∀ {α : Type ?u.38200} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a = c + b → a - b = c
tsub_eq_of_eq_add <| add_comm: ∀ {G : Type ?u.38255} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm a: α
a b: α
b
#align add_le_cancellable.add_tsub_cancel_left AddLECancellable.add_tsub_cancel_left: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b : α}, AddLECancellable a → a + b - a = b
AddLECancellable.add_tsub_cancel_left

protected theorem lt_add_of_tsub_lt_left: ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α}, AddLECancellable b → a - b < c → a < b + c
lt_add_of_tsub_lt_left (hb: AddLECancellable b
hb : AddLECancellable: {α : Type ?u.38483} → [inst : Add α] → [inst : LE α] → α → Prop
AddLECancellable b: α
b) (h: a - b < c
h : a: α
a - b: α
b < c: α
c) : a: α
a < b: α
b + c: α
c := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.38298

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a - b < c

a < b + crw [α: Type u_1

β: Type ?u.38298

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a - b < c

a < b + clt_iff_le_and_ne: ∀ {α : Type ?u.38956} [inst : PartialOrder α] {a b : α}, a < b ↔ a ≤ b ∧ a ≠ b
lt_iff_le_and_ne,α: Type u_1

β: Type ?u.38298

inst✝³: PartialOrder α

inst✝²: AddCommSemigroup α

inst✝¹: Sub α

inst✝: OrderedSub α

a, b, c, d: α

hb: AddLECancellable b

h: a - b < c

a ≤ b + c ∧ a ≠ b + c