Theorems · Theorem · order theory

tsub_add_tsub_comm

∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α], b ≤ a → d ≤ c → a - b + (c - d) = a + c - (b + d)

Defined in

Mathlib.Algebra.Order.Sub.Unbundled.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommSemigroupPartialOrderExistsAddOfLEAddLeftMonoSubOrderedSubAddLeftReflectLE