Lemmas about subtraction in unbundled canonically ordered monoids

theorem AddHom.le_map_tsub {α : Type u_1} {β : Type u_2} [Preorder α] [Add α] [Sub α] [OrderedSub α] [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : α →ₙ+ β) (hf : Monotone ⇑f) (a b : α) : f a - f b ≤ f (a - b)

theorem le_mul_tsub {R : Type u_3} [Distrib R] [Preorder R] [Sub R] [OrderedSub R] [MulLeftMono R] {a b c : R} : a * b - a * c ≤ a * (b - c)

theorem le_tsub_mul {R : Type u_3} [NonUnitalCommSemiring R] [Preorder R] [Sub R] [OrderedSub R] [MulLeftMono R] {a b c : R} : a * c - b * c ≤ (a - b) * c

theorem map_tsub_of_le {α : Type u_1} {β : Type u_2} {F : Type u_3} [PartialOrder α] [AddCommSemigroup α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] [PartialOrder β] [AddCommSemigroup β] [Sub β] [OrderedSub β] [AddLeftReflectLE β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : α) (h : b ≤ a) : f a - f b = f (a - b)

theorem OrderIso.map_tsub {M : Type u_3} {N : Type u_4} [Preorder M] [Add M] [Sub M] [OrderedSub M] [PartialOrder N] [Add N] [Sub N] [OrderedSub N] (e : M ≃o N) (h_add : ∀ (a b : M), e (a + b) = e a + e b) (a b : M) : e (a - b) = e a - e b

An order isomorphism between types with ordered subtraction preserves subtraction provided that it preserves addition.

Preorder

theorem AddMonoidHom.le_map_tsub {α : Type u_1} {β : Type u_2} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] [Preorder β] [AddZeroClass β] [Sub β] [OrderedSub β] (f : α →+ β) (hf : Monotone ⇑f) (a b : α) : f a - f b ≤ f (a - b)