diff --git a/Mathlib.lean b/Mathlib.lean
index c288e312d7466..dfa5d02698df5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -645,9 +645,10 @@ import Mathlib.Algebra.Order.Ring.Unbundled.Basic
 import Mathlib.Algebra.Order.Ring.Unbundled.Nonneg
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Sub.Basic
-import Mathlib.Algebra.Order.Sub.Canonical
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
+import Mathlib.Algebra.Order.Sub.Unbundled.Hom
 import Mathlib.Algebra.Order.Sub.WithTop
 import Mathlib.Algebra.Order.Sum
 import Mathlib.Algebra.Order.ToIntervalMod
@@ -2290,6 +2291,7 @@ import Mathlib.Data.Multiset.Interval
 import Mathlib.Data.Multiset.Lattice
 import Mathlib.Data.Multiset.NatAntidiagonal
 import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Data.Multiset.Pi
 import Mathlib.Data.Multiset.Powerset
 import Mathlib.Data.Multiset.Range
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
index 602f1900802b6..db06873e55a04 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean
@@ -39,6 +39,7 @@ See the documentation of `to_additive.attr` for more information.
 -- assert_not_exists AddCommMonoidWithOne
 assert_not_exists MonoidWithZero
 assert_not_exists MulAction
+assert_not_exists OrderedCommMonoid
 
 variable {ι κ α β γ : Type*}
 
@@ -1455,11 +1456,12 @@ theorem eq_prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
 reduces to the difference of the last and first terms
 when the function we are summing is monotone.
 -/
-theorem sum_range_tsub [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] {f : ℕ → α} (h : Monotone f) (n : ℕ) :
+theorem sum_range_tsub [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α]
+    [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)] [ExistsAddOfLE α]
+    {f : ℕ → α} (h : Monotone f) (n : ℕ) :
     ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0 := by
   apply sum_range_induction
-  case base => apply tsub_self
+  case base => apply tsub_eq_of_eq_add; rw [zero_add]
   case step =>
     intro n
     have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
@@ -1684,7 +1686,7 @@ theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
     exact fun i hi => if_neg (h i hi)
 
 @[to_additive]
-theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [OrderedCommMonoid γ]
+theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [CommMonoid γ] [Preorder γ]
     [CovariantClass γ γ (· * ·) (· < ·)] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ}
     (hdf : 1 < f d) : ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m := by
   conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]
diff --git a/Mathlib/Algebra/Order/Antidiag/Prod.lean b/Mathlib/Algebra/Order/Antidiag/Prod.lean
index dde92767a53bf..6f49ffaa10635 100644
--- a/Mathlib/Algebra/Order/Antidiag/Prod.lean
+++ b/Mathlib/Algebra/Order/Antidiag/Prod.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Antoine Chambert-Loir and María Inés de Frutos-Fernández.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser
 -/
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Data.Finset.Basic
 import Mathlib.Order.Interval.Finset.Defs
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
index ce3eb2fbc4a57..93535400087e6 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Tactic.Bound.Attribute
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.Positivity.Core
diff --git a/Mathlib/Algebra/Order/Field/Pi.lean b/Mathlib/Algebra/Order/Field/Pi.lean
index c0765788d3056..7100886df9c3c 100644
--- a/Mathlib/Algebra/Order/Field/Pi.lean
+++ b/Mathlib/Algebra/Order/Field/Pi.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Data.Finset.Lattice
 import Mathlib.Data.Fintype.Card
 
diff --git a/Mathlib/Algebra/Order/Ring/Canonical.lean b/Mathlib/Algebra/Order/Ring/Canonical.lean
index 432f79a5c6202..1f64f689d1e79 100644
--- a/Mathlib/Algebra/Order/Ring/Canonical.lean
+++ b/Mathlib/Algebra/Order/Ring/Canonical.lean
@@ -3,8 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Ring.Defs
-import Mathlib.Algebra.Order.Sub.Canonical
+import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Ring.Parity
 
 /-!
diff --git a/Mathlib/Algebra/Order/Sub/Basic.lean b/Mathlib/Algebra/Order/Sub/Basic.lean
index dbd995c294236..79046c54164c0 100644
--- a/Mathlib/Algebra/Order/Sub/Basic.lean
+++ b/Mathlib/Algebra/Order/Sub/Basic.lean
@@ -3,58 +3,199 @@ 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
 -/
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Order.Sub.Defs
-import Mathlib.Order.Hom.Basic
-
+import Mathlib.Algebra.Group.Even
 /-!
-# Additional results about ordered Subtraction
-
+# Lemmas about subtraction in unbundled canonically ordered monoids
 -/
 
+variable {α : Type*}
+
+section CanonicallyOrderedAddCommMonoid
+
+variable [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+
+theorem add_tsub_cancel_iff_le : a + (b - a) = b ↔ a ≤ b :=
+  ⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩
+
+theorem tsub_add_cancel_iff_le : b - a + a = b ↔ a ≤ b := by
+  rw [add_comm]
+  exact add_tsub_cancel_iff_le
+
+-- This was previously a `@[simp]` lemma, but it is not necessarily a good idea, e.g. in
+-- `example (h : n - m = 0) : a + (n - m) = a := by simp_all`
+theorem tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b := by
+  rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
+
+alias ⟨_, tsub_eq_zero_of_le⟩ := tsub_eq_zero_iff_le
+
+attribute [simp] tsub_eq_zero_of_le
+
+theorem tsub_self (a : α) : a - a = 0 :=
+  tsub_eq_zero_of_le le_rfl
+
+theorem tsub_le_self : a - b ≤ a :=
+  tsub_le_iff_left.mpr <| le_add_left le_rfl
+
+theorem zero_tsub (a : α) : 0 - a = 0 :=
+  tsub_eq_zero_of_le <| zero_le a
+
+theorem tsub_self_add (a b : α) : a - (a + b) = 0 :=
+  tsub_eq_zero_of_le <| self_le_add_right _ _
+
+theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b := by
+  rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
+
+theorem tsub_pos_of_lt (h : a < b) : 0 < b - a :=
+  tsub_pos_iff_not_le.mpr h.not_le
+
+theorem tsub_lt_of_lt (h : a < b) : a - c < b :=
+  lt_of_le_of_lt tsub_le_self h
+
+namespace AddLECancellable
+
+protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c)
+    (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b := by
+  refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
+  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
+    add_comm b]
+  apply ha
+
+protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
+    (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
+  simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
+    and_comm]
+
+end AddLECancellable
+
+/-! #### Lemmas where addition is order-reflecting. -/
+
+
+section Contra
+
+variable [ContravariantClass α α (· + ·) (· ≤ ·)]
+
+theorem tsub_le_tsub_iff_left (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b :=
+  Contravariant.AddLECancellable.tsub_le_tsub_iff_left Contravariant.AddLECancellable h
+
+theorem tsub_right_inj (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c :=
+  Contravariant.AddLECancellable.tsub_right_inj Contravariant.AddLECancellable
+    Contravariant.AddLECancellable hba hca
+
+variable (α)
+
+/-- A `CanonicallyOrderedAddCommMonoid` with ordered subtraction and order-reflecting addition is
+cancellative. This is not an instance as it would form a typeclass loop.
+
+See note [reducible non-instances]. -/
+abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid : AddCancelCommMonoid α :=
+  { (by infer_instance : AddCommMonoid α) with
+    add_left_cancel := fun a b c h => by
+      simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h }
+
+end Contra
+
+end CanonicallyOrderedAddCommMonoid
+
+/-! ### Lemmas in a linearly canonically ordered monoid. -/
+
+
+section CanonicallyLinearOrderedAddCommMonoid
+
+variable [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+
+@[simp]
+theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a := by rw [tsub_pos_iff_not_le, not_le]
+
+theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
+  · rw [min_eq_right h]
+
+namespace AddLECancellable
+
+protected theorem lt_tsub_iff_right (hc : AddLECancellable c) : a < b - c ↔ a + c < b :=
+  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_right.mpr, hc.lt_tsub_of_add_lt_right⟩
+
+protected theorem lt_tsub_iff_left (hc : AddLECancellable c) : a < b - c ↔ c + a < b :=
+  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩
+
+protected theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) :
+    a - c < b - c ↔ a < b := by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
+
+protected theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a := by
+  refine tsub_le_self.lt_of_ne fun h => ?_
+  rw [← h, tsub_pos_iff_lt] at h₁
+  exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)
+
+protected theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b := by
+  refine
+    ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
+  rintro rfl
+  rw [tsub_zero] at h
+  exact h.false
+
+/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
+protected theorem tsub_lt_tsub_iff_left_of_le (ha : AddLECancellable a) (hb : AddLECancellable b)
+    (h : b ≤ a) : a - b < a - c ↔ c < b :=
+  lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h
+
+end AddLECancellable
+
+section Contra
+
+variable [ContravariantClass α α (· + ·) (· ≤ ·)]
 
-variable {α β : Type*}
+/-- This lemma also holds for `ENNReal`, but we need a different proof for that. -/
+theorem tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
+  Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h
 
-section Add
+theorem tsub_lt_self : 0 < a → 0 < b → a - b < a :=
+  Contravariant.AddLECancellable.tsub_lt_self
 
-variable [Preorder α] [Add α] [Sub α] [OrderedSub α] {a b c d : α}
+@[simp] theorem tsub_lt_self_iff : a - b < a ↔ 0 < a ∧ 0 < b :=
+  Contravariant.AddLECancellable.tsub_lt_self_iff
 
-theorem AddHom.le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β)
-    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) := by
-  rw [tsub_le_iff_right, ← f.map_add]
-  exact hf le_tsub_add
+/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
+theorem tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=
+  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h
 
-theorem le_mul_tsub {R : Type*} [Distrib R] [Preorder R] [Sub R] [OrderedSub R]
-    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * b - a * c ≤ a * (b - c) :=
-  (AddHom.mulLeft a).le_map_tsub (monotone_id.const_mul' a) _ _
+lemma tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b := by
+  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
 
-theorem le_tsub_mul {R : Type*} [CommSemiring R] [Preorder R] [Sub R] [OrderedSub R]
-    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * c - b * c ≤ (a - b) * c := by
-  simpa only [mul_comm _ c] using le_mul_tsub
+end Contra
 
-end Add
+/-! ### Lemmas about `max` and `min`. -/
 
-/-- An order isomorphism between types with ordered subtraction preserves subtraction provided that
-it preserves addition. -/
-theorem OrderIso.map_tsub {M N : Type*} [Preorder M] [Add M] [Sub M] [OrderedSub M]
-    [PartialOrder N] [Add N] [Sub N] [OrderedSub N] (e : M ≃o N)
-    (h_add : ∀ a b, e (a + b) = e a + e b) (a b : M) : e (a - b) = e a - e b := by
-  let e_add : M ≃+ N := { e with map_add' := h_add }
-  refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)
-  suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
-  exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
 
-/-! ### Preorder -/
+theorem tsub_add_eq_max : a - b + b = max a b := by
+  rcases le_total a b with h | h
+  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
+  · rw [max_eq_left h, tsub_add_cancel_of_le h]
 
+theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, tsub_add_eq_max]
 
-section Preorder
+theorem tsub_min : a - min a b = a - b := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
+  · rw [min_eq_right h]
 
-variable [Preorder α]
-variable [AddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+theorem tsub_add_min : a - b + min a b = a := by
+  rw [← tsub_min, @tsub_add_cancel_of_le]
+  apply min_le_left
 
-theorem AddMonoidHom.le_map_tsub [Preorder β] [AddCommMonoid β] [Sub β] [OrderedSub β] (f : α →+ β)
-    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) :=
-  f.toAddHom.le_map_tsub hf a b
+-- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
+lemma Even.tsub
+    [ContravariantClass α α (· + ·) (· ≤ ·)] {m n : α} (hm : Even m) (hn : Even n) :
+    Even (m - n) := by
+  obtain ⟨a, rfl⟩ := hm
+  obtain ⟨b, rfl⟩ := hn
+  refine ⟨a - b, ?_⟩
+  obtain h | h := le_total a b
+  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
+  · exact (tsub_add_tsub_comm h h).symm
 
-end Preorder
+end CanonicallyLinearOrderedAddCommMonoid
diff --git a/Mathlib/Algebra/Order/Sub/Canonical.lean b/Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
similarity index 60%
rename from Mathlib/Algebra/Order/Sub/Canonical.lean
rename to Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
index f8591c56f68d8..979e4903eb48f 100644
--- a/Mathlib/Algebra/Order/Sub/Canonical.lean
+++ b/Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
@@ -3,14 +3,15 @@ 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
 -/
-import Mathlib.Algebra.Group.Even
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Sub.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 
 /-!
-# Lemmas about subtraction in canonically ordered monoids
+# Lemmas about subtraction in an unbundled canonically ordered monoids
 -/
 
+-- These are about *unbundled* canonically ordered monoids
+assert_not_exists OrderedCommMonoid
 
 variable {α : Type*}
 
@@ -255,192 +256,3 @@ theorem tsub_tsub_eq_add_tsub_of_le
 end Contra
 
 end ExistsAddOfLE
-
-/-! ### Lemmas in a canonically ordered monoid. -/
-
-
-section CanonicallyOrderedAddCommMonoid
-
-variable [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
-
-theorem add_tsub_cancel_iff_le : a + (b - a) = b ↔ a ≤ b :=
-  ⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩
-
-theorem tsub_add_cancel_iff_le : b - a + a = b ↔ a ≤ b := by
-  rw [add_comm]
-  exact add_tsub_cancel_iff_le
-
--- This was previously a `@[simp]` lemma, but it is not necessarily a good idea, e.g. in
--- `example (h : n - m = 0) : a + (n - m) = a := by simp_all`
-theorem tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b := by
-  rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
-
-alias ⟨_, tsub_eq_zero_of_le⟩ := tsub_eq_zero_iff_le
-
-attribute [simp] tsub_eq_zero_of_le
-
-theorem tsub_self (a : α) : a - a = 0 :=
-  tsub_eq_zero_of_le le_rfl
-
-theorem tsub_le_self : a - b ≤ a :=
-  tsub_le_iff_left.mpr <| le_add_left le_rfl
-
-theorem zero_tsub (a : α) : 0 - a = 0 :=
-  tsub_eq_zero_of_le <| zero_le a
-
-theorem tsub_self_add (a b : α) : a - (a + b) = 0 :=
-  tsub_eq_zero_of_le <| self_le_add_right _ _
-
-theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b := by
-  rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
-
-theorem tsub_pos_of_lt (h : a < b) : 0 < b - a :=
-  tsub_pos_iff_not_le.mpr h.not_le
-
-theorem tsub_lt_of_lt (h : a < b) : a - c < b :=
-  lt_of_le_of_lt tsub_le_self h
-
-namespace AddLECancellable
-
-protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c)
-    (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b := by
-  refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
-  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
-    add_comm b]
-  apply ha
-
-protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
-    (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
-  simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
-    and_comm]
-
-end AddLECancellable
-
-/-! #### Lemmas where addition is order-reflecting. -/
-
-
-section Contra
-
-variable [ContravariantClass α α (· + ·) (· ≤ ·)]
-
-theorem tsub_le_tsub_iff_left (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b :=
-  Contravariant.AddLECancellable.tsub_le_tsub_iff_left Contravariant.AddLECancellable h
-
-theorem tsub_right_inj (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c :=
-  Contravariant.AddLECancellable.tsub_right_inj Contravariant.AddLECancellable
-    Contravariant.AddLECancellable hba hca
-
-variable (α)
-
-/-- A `CanonicallyOrderedAddCommMonoid` with ordered subtraction and order-reflecting addition is
-cancellative. This is not an instance as it would form a typeclass loop.
-
-See note [reducible non-instances]. -/
-abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid : AddCancelCommMonoid α :=
-  { (by infer_instance : AddCommMonoid α) with
-    add_left_cancel := fun a b c h => by
-      simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h }
-
-end Contra
-
-end CanonicallyOrderedAddCommMonoid
-
-/-! ### Lemmas in a linearly canonically ordered monoid. -/
-
-
-section CanonicallyLinearOrderedAddCommMonoid
-
-variable [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
-
-@[simp]
-theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a := by rw [tsub_pos_iff_not_le, not_le]
-
-theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b := by
-  rcases le_total a b with h | h
-  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
-  · rw [min_eq_right h]
-
-namespace AddLECancellable
-
-protected theorem lt_tsub_iff_right (hc : AddLECancellable c) : a < b - c ↔ a + c < b :=
-  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_right.mpr, hc.lt_tsub_of_add_lt_right⟩
-
-protected theorem lt_tsub_iff_left (hc : AddLECancellable c) : a < b - c ↔ c + a < b :=
-  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩
-
-protected theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) :
-    a - c < b - c ↔ a < b := by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
-
-protected theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a := by
-  refine tsub_le_self.lt_of_ne fun h => ?_
-  rw [← h, tsub_pos_iff_lt] at h₁
-  exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)
-
-protected theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b := by
-  refine
-    ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
-  rintro rfl
-  rw [tsub_zero] at h
-  exact h.false
-
-/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
-protected theorem tsub_lt_tsub_iff_left_of_le (ha : AddLECancellable a) (hb : AddLECancellable b)
-    (h : b ≤ a) : a - b < a - c ↔ c < b :=
-  lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h
-
-end AddLECancellable
-
-section Contra
-
-variable [ContravariantClass α α (· + ·) (· ≤ ·)]
-
-/-- This lemma also holds for `ENNReal`, but we need a different proof for that. -/
-theorem tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
-  Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h
-
-theorem tsub_lt_self : 0 < a → 0 < b → a - b < a :=
-  Contravariant.AddLECancellable.tsub_lt_self
-
-@[simp] theorem tsub_lt_self_iff : a - b < a ↔ 0 < a ∧ 0 < b :=
-  Contravariant.AddLECancellable.tsub_lt_self_iff
-
-/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
-theorem tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=
-  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h
-
-lemma tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b := by
-  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
-
-end Contra
-
-/-! ### Lemmas about `max` and `min`. -/
-
-
-theorem tsub_add_eq_max : a - b + b = max a b := by
-  rcases le_total a b with h | h
-  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
-  · rw [max_eq_left h, tsub_add_cancel_of_le h]
-
-theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, tsub_add_eq_max]
-
-theorem tsub_min : a - min a b = a - b := by
-  rcases le_total a b with h | h
-  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
-  · rw [min_eq_right h]
-
-theorem tsub_add_min : a - b + min a b = a := by
-  rw [← tsub_min, @tsub_add_cancel_of_le]
-  apply min_le_left
-
--- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
-lemma Even.tsub
-    [ContravariantClass α α (· + ·) (· ≤ ·)] {m n : α} (hm : Even m) (hn : Even n) :
-    Even (m - n) := by
-  obtain ⟨a, rfl⟩ := hm
-  obtain ⟨b, rfl⟩ := hn
-  refine ⟨a - b, ?_⟩
-  obtain h | h := le_total a b
-  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
-  · exact (tsub_add_tsub_comm h h).symm
-
-end CanonicallyLinearOrderedAddCommMonoid
diff --git a/Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean b/Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean
new file mode 100644
index 0000000000000..2bf9585fa56a6
--- /dev/null
+++ b/Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean
@@ -0,0 +1,58 @@
+/-
+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
+-/
+import Mathlib.Algebra.Order.Sub.Defs
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Algebra.Ring.Basic
+import Mathlib.Order.Hom.Basic
+/-!
+# Lemmas about subtraction in unbundled canonically ordered monoids
+-/
+
+
+variable {α β : Type*}
+
+section Add
+
+variable [Preorder α] [Add α] [Sub α] [OrderedSub α] {a b c d : α}
+
+theorem AddHom.le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β)
+    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) := by
+  rw [tsub_le_iff_right, ← f.map_add]
+  exact hf le_tsub_add
+
+theorem le_mul_tsub {R : Type*} [Distrib R] [Preorder R] [Sub R] [OrderedSub R]
+    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * b - a * c ≤ a * (b - c) :=
+  (AddHom.mulLeft a).le_map_tsub (monotone_id.const_mul' a) _ _
+
+theorem le_tsub_mul {R : Type*} [CommSemiring R] [Preorder R] [Sub R] [OrderedSub R]
+    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * c - b * c ≤ (a - b) * c := by
+  simpa only [mul_comm _ c] using le_mul_tsub
+
+end Add
+
+/-- An order isomorphism between types with ordered subtraction preserves subtraction provided that
+it preserves addition. -/
+theorem OrderIso.map_tsub {M N : Type*} [Preorder M] [Add M] [Sub M] [OrderedSub M]
+    [PartialOrder N] [Add N] [Sub N] [OrderedSub N] (e : M ≃o N)
+    (h_add : ∀ a b, e (a + b) = e a + e b) (a b : M) : e (a - b) = e a - e b := by
+  let e_add : M ≃+ N := { e with map_add' := h_add }
+  refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)
+  suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
+  exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
+
+/-! ### Preorder -/
+
+
+section Preorder
+
+variable [Preorder α]
+variable [AddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+
+theorem AddMonoidHom.le_map_tsub [Preorder β] [AddCommMonoid β] [Sub β] [OrderedSub β] (f : α →+ β)
+    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) :=
+  f.toAddHom.le_map_tsub hf a b
+
+end Preorder
diff --git a/Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean b/Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
index a2b9e02f3bc43..4cef85d6ad0d3 100644
--- a/Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
+++ b/Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
@@ -120,7 +120,7 @@ theorem antidiagonalTuple_zero_right : ∀ k, antidiagonalTuple k 0 = [0]
 @[simp]
 theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = [![n]] := by
   simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
-    tsub_self, List.bind_append, List.bind_singleton, List.bind_map]
+    Nat.sub_self, List.bind_append, List.bind_singleton, List.bind_map]
   conv_rhs => rw [← List.nil_append [![n]]]
   congr 1
   simp_rw [List.bind_eq_nil, List.mem_range, List.map_eq_nil]
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
index bd963644daca7..e421e88c289c7 100644
--- a/Mathlib/Data/Finset/Basic.lean
+++ b/Mathlib/Data/Finset/Basic.lean
@@ -122,6 +122,8 @@ assert_not_exists Multiset.powerset
 
 assert_not_exists CompleteLattice
 
+assert_not_exists OrderedCommMonoid
+
 open Multiset Subtype Nat Function
 
 universe u
@@ -1745,7 +1747,7 @@ variable [DecidableEq α] {s t u v : Finset α} {a b : α}
 
 /-- `s \ t` is the set consisting of the elements of `s` that are not in `t`. -/
 instance : SDiff (Finset α) :=
-  ⟨fun s₁ s₂ => ⟨s₁.1 - s₂.1, nodup_of_le tsub_le_self s₁.2⟩⟩
+  ⟨fun s₁ s₂ => ⟨s₁.1 - s₂.1, nodup_of_le (Multiset.sub_le_self ..) s₁.2⟩⟩
 
 @[simp]
 theorem sdiff_val (s₁ s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val :=
@@ -2580,7 +2582,7 @@ theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then
 
 lemma range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial := by
   rw [Finset.Nontrivial, Finset.coe_range]
-  exact ⟨0, Nat.zero_lt_one.trans hn, 1, hn, zero_ne_one⟩
+  exact ⟨0, Nat.zero_lt_one.trans hn, 1, hn, Nat.zero_ne_one⟩
 
 end Range
 
diff --git a/Mathlib/Data/Finset/Fold.lean b/Mathlib/Data/Finset/Fold.lean
index 06a0145f30d7f..39befbf6c8239 100644
--- a/Mathlib/Data/Finset/Fold.lean
+++ b/Mathlib/Data/Finset/Fold.lean
@@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Multiset.Fold
-import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 
 /-!
 # The fold operation for a commutative associative operation over a finset.
 -/
 
--- TODO:
--- assert_not_exists OrderedCommMonoid
+assert_not_exists OrderedCommMonoid
 assert_not_exists MonoidWithZero
 
 namespace Finset
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
index 16acc98aceb59..9cb9fd5e3090c 100644
--- a/Mathlib/Data/Finset/Lattice.lean
+++ b/Mathlib/Data/Finset/Lattice.lean
@@ -19,7 +19,7 @@ import Mathlib.Order.Nat
 -/
 
 -- TODO:
--- assert_not_exists OrderedCommMonoid
+assert_not_exists OrderedCommMonoid
 assert_not_exists MonoidWithZero
 
 open Function Multiset OrderDual
@@ -812,8 +812,9 @@ theorem _root_.map_finset_sup' [SemilatticeSup β] [FunLike F α β] [SupHomClas
     f (s.sup' hs g) = s.sup' hs (f ∘ g) := by
   refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]
 
-lemma nsmul_sup' {α'} [LinearOrderedAddCommMonoid β] {s : Finset α'}
-    (hs : s.Nonempty) (f : α' → β) (n : ℕ) :
+lemma nsmul_sup' {α β : Type*} [AddMonoid β] [LinearOrder β]
+    [CovariantClass β β (· + ·) (· ≤ ·)] [CovariantClass β β (swap (· + ·)) (· ≤ ·)]
+    {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) :
     s.sup' hs (fun a => n • f a) = n • s.sup' hs f :=
   let ns : SupHom β β := { toFun := (n • ·), map_sup' := fun _ _ => (nsmul_right_mono n).map_max }
   (map_finset_sup' ns hs _).symm
@@ -963,8 +964,9 @@ theorem _root_.map_finset_inf' [SemilatticeInf β] [FunLike F α β] [InfHomClas
     f (s.inf' hs g) = s.inf' hs (f ∘ g) := by
   refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]
 
-lemma nsmul_inf' {α'} [LinearOrderedAddCommMonoid β] {s : Finset α'}
-    (hs : s.Nonempty) (f : α' → β) (n : ℕ) :
+lemma nsmul_inf' {α β : Type*} [AddMonoid β] [LinearOrder β]
+    [CovariantClass β β (· + ·) (· ≤ ·)] [CovariantClass β β (swap (· + ·)) (· ≤ ·)]
+    {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) :
     s.inf' hs (fun a => n • f a) = n • s.inf' hs f :=
   let ns : InfHom β β := { toFun := (n • ·), map_inf' := fun _ _ => (nsmul_right_mono n).map_min }
   (map_finset_inf' ns hs _).symm
diff --git a/Mathlib/Data/Finset/MulAntidiagonal.lean b/Mathlib/Data/Finset/MulAntidiagonal.lean
index 6d9a95ba9eb9e..683d02323b1ff 100644
--- a/Mathlib/Data/Finset/MulAntidiagonal.lean
+++ b/Mathlib/Data/Finset/MulAntidiagonal.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yaël Dillies
 -/
+import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Data.Set.MulAntidiagonal
 
diff --git a/Mathlib/Data/Finset/NatAntidiagonal.lean b/Mathlib/Data/Finset/NatAntidiagonal.lean
index 012eccf69ede9..c5cb7f832ea29 100644
--- a/Mathlib/Data/Finset/NatAntidiagonal.lean
+++ b/Mathlib/Data/Finset/NatAntidiagonal.lean
@@ -151,7 +151,7 @@ theorem antidiagonal.snd_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagon
 def antidiagonalEquivFin (n : ℕ) : antidiagonal n ≃ Fin (n + 1) where
   toFun := fun ⟨⟨i, j⟩, h⟩ ↦ ⟨i, antidiagonal.fst_lt h⟩
   invFun := fun ⟨i, h⟩ ↦ ⟨⟨i, n - i⟩, by
-    rw [mem_antidiagonal, add_comm, tsub_add_cancel_iff_le]
+    rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]
     exact Nat.le_of_lt_succ h⟩
   left_inv := by rintro ⟨⟨i, j⟩, h⟩; ext; rfl
   right_inv x := rfl
diff --git a/Mathlib/Data/Int/Interval.lean b/Mathlib/Data/Int/Interval.lean
index 39cd170eb6188..a0d03d9652740 100644
--- a/Mathlib/Data/Int/Interval.lean
+++ b/Mathlib/Data/Int/Interval.lean
@@ -182,7 +182,7 @@ theorem image_Ico_emod (n a : ℤ) (h : 0 ≤ a) : (Ico n (n + a)).image (· % a
     · exact hn.symm.le.trans (add_le_add_right hi _)
     · rw [add_comm n a]
       refine add_lt_add_of_lt_of_le hia.right (le_trans ?_ hn.le)
-      simp only [zero_le, le_add_iff_nonneg_left]
+      simp only [Nat.zero_le, le_add_iff_nonneg_left]
       exact Int.emod_nonneg n (ne_of_gt ha)
     · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]
 
diff --git a/Mathlib/Data/Multiset/Antidiagonal.lean b/Mathlib/Data/Multiset/Antidiagonal.lean
index f74172f629ecb..df02ceb0f2f41 100644
--- a/Mathlib/Data/Multiset/Antidiagonal.lean
+++ b/Mathlib/Data/Multiset/Antidiagonal.lean
@@ -12,6 +12,7 @@ The antidiagonal of a multiset `s` consists of all pairs `(t₁, t₂)`
 such that `t₁ + t₂ = s`. These pairs are counted with multiplicities.
 -/
 
+assert_not_exists OrderedCommMonoid
 assert_not_exists Ring
 
 universe u
@@ -80,7 +81,7 @@ theorem antidiagonal_cons (a : α) (s) :
 theorem antidiagonal_eq_map_powerset [DecidableEq α] (s : Multiset α) :
     s.antidiagonal = s.powerset.map fun t ↦ (s - t, t) := by
   induction' s using Multiset.induction_on with a s hs
-  · simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton]
+  · simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]
   · simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_mk,
       id, sub_cons, erase_cons_head]
     rw [add_comm]
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
index 6889f2116d1eb..2c9d3259722e0 100644
--- a/Mathlib/Data/Multiset/Basic.lean
+++ b/Mathlib/Data/Multiset/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Nat
-import Mathlib.Algebra.Order.Sub.Canonical
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 import Mathlib.Data.List.Perm
 import Mathlib.Data.Set.List
 import Mathlib.Init.Quot
@@ -17,6 +17,9 @@ These are implemented as the quotient of a list by permutations.
 We define the global infix notation `::ₘ` for `Multiset.cons`.
 -/
 
+-- No bundled ordered algebra should be required
+assert_not_exists OrderedCommMonoid
+
 universe v
 
 open List Subtype Nat Function
@@ -585,16 +588,14 @@ instance : CovariantClass (Multiset α) (Multiset α) (· + ·) (· ≤ ·) :=
 instance : ContravariantClass (Multiset α) (Multiset α) (· + ·) (· ≤ ·) :=
   ⟨fun _s _t _u => add_le_add_iff_left'.1⟩
 
-instance : OrderedCancelAddCommMonoid (Multiset α) where
-  zero := 0
-  add := (· + ·)
+instance instAddCommMonoid : AddCancelCommMonoid (Multiset α) where
   add_comm := fun s t => Quotient.inductionOn₂ s t fun l₁ l₂ => Quot.sound perm_append_comm
   add_assoc := fun s₁ s₂ s₃ =>
     Quotient.inductionOn₃ s₁ s₂ s₃ fun l₁ l₂ l₃ => congr_arg _ <| append_assoc l₁ l₂ l₃
   zero_add := fun s => Quot.inductionOn s fun l => rfl
   add_zero := fun s => Quotient.inductionOn s fun l => congr_arg _ <| append_nil l
-  add_le_add_left := fun s₁ s₂ => add_le_add_left
-  le_of_add_le_add_left := fun s₁ s₂ s₃ => le_of_add_le_add_left
+  add_left_cancel := fun _ _ _ h =>
+    le_antisymm (Multiset.add_le_add_iff_left'.mp h.le) (Multiset.add_le_add_iff_left'.mp h.ge)
   nsmul := nsmulRec
 
 theorem le_add_right (s t : Multiset α) : s ≤ s + t := by simpa using add_le_add_left (zero_le t) s
@@ -608,13 +609,6 @@ theorem le_iff_exists_add {s t : Multiset α} : s ≤ t ↔ ∃ u, t = s + u :=
       ⟨l, Quot.sound p⟩,
     fun ⟨_u, e⟩ => e.symm ▸ le_add_right _ _⟩
 
-instance : CanonicallyOrderedAddCommMonoid (Multiset α) where
-  __ := inferInstanceAs (OrderBot (Multiset α))
-  le_self_add := le_add_right
-  exists_add_of_le h := leInductionOn h fun s =>
-      let ⟨l, p⟩ := s.exists_perm_append
-      ⟨l, Quot.sound p⟩
-
 @[simp]
 theorem cons_add (a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t) := by
   rw [← singleton_add, ← singleton_add, add_assoc]
@@ -1446,6 +1440,9 @@ protected theorem sub_zero (s : Multiset α) : s - 0 = s :=
 theorem sub_cons (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t :=
   Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ <| diff_cons _ _ _
 
+protected theorem zero_sub (t : Multiset α) : 0 - t = 0 :=
+  Multiset.induction_on t rfl fun a s ih => by simp [ih]
+
 /-- This is a special case of `tsub_le_iff_right`, which should be used instead of this.
   This is needed to prove `OrderedSub (Multiset α)`. -/
 protected theorem sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by
@@ -1453,9 +1450,18 @@ protected theorem sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by
   exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by
       simp [IH, erase_le_iff_le_cons])
 
+protected theorem sub_le_self (s t : Multiset α) : s - t ≤ s := by
+  rw [Multiset.sub_le_iff_le_add]
+  exact le_add_right _ _
+
 instance : OrderedSub (Multiset α) :=
   ⟨fun _n _m _k => Multiset.sub_le_iff_le_add⟩
 
+instance : ExistsAddOfLE (Multiset α) where
+  exists_add_of_le h := leInductionOn h fun s =>
+      let ⟨l, p⟩ := s.exists_perm_append
+      ⟨l, Quot.sound p⟩
+
 theorem cons_sub_of_le (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t) := by
   rw [← singleton_add, ← singleton_add, add_tsub_assoc_of_le h]
 
@@ -1500,9 +1506,10 @@ theorem union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u :=
 theorem union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by
   rw [← eq_union_left h₂]; exact union_le_union_right h₁ t
 
+
 @[simp]
 theorem mem_union : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t :=
-  ⟨fun h => (mem_add.1 h).imp_left (mem_of_le tsub_le_self),
+  ⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _),
     (Or.elim · (mem_of_le <| le_union_left _ _) (mem_of_le <| le_union_right _ _))⟩
 
 @[simp]
@@ -1512,7 +1519,7 @@ theorem map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f)
     congr_arg ofList (by rw [List.map_append f, List.map_diff finj])
 
 @[simp] theorem zero_union : 0 ∪ s = s := by
-  simp [union_def]
+  simp [union_def, Multiset.zero_sub]
 
 @[simp] theorem union_zero : s ∪ 0 = s := by
   simp [union_def]
@@ -1554,7 +1561,7 @@ theorem inter_le_right (s : Multiset α) : ∀ t, s ∩ t ≤ t :=
 
 theorem le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u := by
   revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂
-  · simpa only [zero_inter, nonpos_iff_eq_zero] using h₁
+  · simpa only [zero_inter] using h₁
   by_cases h : a ∈ u
   · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
     exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
diff --git a/Mathlib/Data/Multiset/Nodup.lean b/Mathlib/Data/Multiset/Nodup.lean
index 7e24031fb1f8c..2ea7505ae7caa 100644
--- a/Mathlib/Data/Multiset/Nodup.lean
+++ b/Mathlib/Data/Multiset/Nodup.lean
@@ -192,7 +192,7 @@ theorem range_le {m n : ℕ} : range m ≤ range n ↔ m ≤ n :=
 theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) :
     a ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
   ⟨fun h =>
-    ⟨mem_of_le tsub_le_self h, fun h' => by
+    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' => by
       refine count_eq_zero.1 ?_ h
       rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
       exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
diff --git a/Mathlib/Data/Multiset/OrderedMonoid.lean b/Mathlib/Data/Multiset/OrderedMonoid.lean
new file mode 100644
index 0000000000000..bf40bc0b213eb
--- /dev/null
+++ b/Mathlib/Data/Multiset/OrderedMonoid.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Data.Multiset.Basic
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+
+/-!
+# Multisets as ordered monoids
+
+The `OrderedCancelAddCommMonoid` and `CanonicallyOrderedAddCommMonoid` instances on `Multiset α`
+
+-/
+
+variable {α : Type*}
+
+namespace Multiset
+
+open List
+
+instance : OrderedCancelAddCommMonoid (Multiset α) where
+  add_le_add_left := fun _ _ => add_le_add_left
+  le_of_add_le_add_left := fun _ _ _ => le_of_add_le_add_left
+
+instance : CanonicallyOrderedAddCommMonoid (Multiset α) where
+  __ := inferInstanceAs (OrderBot (Multiset α))
+  le_self_add := le_add_right
+  exists_add_of_le h := exists_add_of_le h
+
+end Multiset
diff --git a/Mathlib/Data/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean
index 32cae0329ae6c..103a0f6a9d279 100644
--- a/Mathlib/Data/PNat/Factors.lean
+++ b/Mathlib/Data/PNat/Factors.lean
@@ -6,6 +6,7 @@ Authors: Neil Strickland
 import Mathlib.Algebra.BigOperators.Group.Multiset
 import Mathlib.Data.PNat.Prime
 import Mathlib.Data.Nat.Factors
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Data.Multiset.Sort
 
 /-!
diff --git a/Mathlib/Data/Set/MulAntidiagonal.lean b/Mathlib/Data/Set/MulAntidiagonal.lean
index b6b66e2d2c290..487d0d5850eb3 100644
--- a/Mathlib/Data/Set/MulAntidiagonal.lean
+++ b/Mathlib/Data/Set/MulAntidiagonal.lean
@@ -83,7 +83,9 @@ end CancelCommMonoid
 
 section OrderedCancelCommMonoid
 
-variable [OrderedCancelCommMonoid α] (s t : Set α) (a : α) {x y : mulAntidiagonal s t a}
+variable [CancelCommMonoid α] [PartialOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (Function.swap (· * ·)) (· < ·)]
+  (s t : Set α) (a : α) {x y : mulAntidiagonal s t a}
 
 @[to_additive Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd]
 theorem eq_of_fst_le_fst_of_snd_le_snd (h₁ : (x : α × α).1 ≤ (y : α × α).1)
@@ -110,8 +112,11 @@ theorem finite_of_isPWO (hs : s.IsPWO) (ht : t.IsPWO) (a) : (mulAntidiagonal s t
 
 end OrderedCancelCommMonoid
 
+variable [CancelCommMonoid α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (Function.swap (· * ·)) (· < ·)]
+
 @[to_additive Set.AddAntidiagonal.finite_of_isWF]
-theorem finite_of_isWF [LinearOrderedCancelCommMonoid α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF)
+theorem finite_of_isWF {s t : Set α} (hs : s.IsWF) (ht : t.IsWF)
     (a) : (mulAntidiagonal s t a).Finite :=
   finite_of_isPWO hs.isPWO ht.isPWO a
 
diff --git a/Mathlib/GroupTheory/MonoidLocalization/Order.lean b/Mathlib/GroupTheory/MonoidLocalization/Order.lean
index c25bc39fbfb7a..ccdd1707f6e4d 100644
--- a/Mathlib/GroupTheory/MonoidLocalization/Order.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization/Order.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Amelia Livingston
 -/
+import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.GroupTheory.MonoidLocalization.Basic
 
 /-!
diff --git a/Mathlib/RingTheory/HahnSeries/Basic.lean b/Mathlib/RingTheory/HahnSeries/Basic.lean
index b189d32690b7d..b063204680d7f 100644
--- a/Mathlib/RingTheory/HahnSeries/Basic.lean
+++ b/Mathlib/RingTheory/HahnSeries/Basic.lean
@@ -321,7 +321,7 @@ theorem coeff_order_ne_zero {x : HahnSeries Γ R} (hx : x ≠ 0) : x.coeff x.ord
   rw [order_of_ne hx]
   exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)
 
-theorem order_le_of_coeff_ne_zero {Γ} [LinearOrderedCancelAddCommMonoid Γ] {x : HahnSeries Γ R}
+theorem order_le_of_coeff_ne_zero {Γ} [AddMonoid Γ] [LinearOrder Γ] {x : HahnSeries Γ R}
     {g : Γ} (h : x.coeff g ≠ 0) : x.order ≤ g :=
   le_trans (le_of_eq (order_of_ne (ne_zero_of_coeff_ne_zero h)))
     (Set.IsWF.min_le _ _ ((mem_support _ _).2 h))
diff --git a/Mathlib/Tactic/Monotonicity/Lemmas.lean b/Mathlib/Tactic/Monotonicity/Lemmas.lean
index 3ad48a50d8db3..a0ad5266eac62 100644
--- a/Mathlib/Tactic/Monotonicity/Lemmas.lean
+++ b/Mathlib/Tactic/Monotonicity/Lemmas.lean
@@ -5,7 +5,7 @@ Authors: Simon Hudon
 -/
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Ring.Defs
-import Mathlib.Algebra.Order.Sub.Canonical
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 import Mathlib.Data.Set.Lattice
 import Mathlib.Tactic.Monotonicity.Attr