chore(algebra/order/sub): Generalize to preorder and `add_comm_semi…

…group` (#11463)

This generalizes a bunch of lemmas from `partial_order` to `preorder` and from `add_comm_monoid` to `add_comm_semigroup`.

It also adds `tsub_tsub_le_tsub_add : a - (b - c) ≤ a - b + c`.

src/algebra/order/sub.lean

@@ -92,11 +92,15 @@ begin
   exact e.monotone (e_add.symm.to_add_hom.le_map_tsub e.symm.monotone _ _)
 end
 
+/-! ### Preorder -/
+
 section ordered_add_comm_monoid
 
 section preorder
+variables [preorder α]
 
-variables [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α}
+section add_comm_semigroup
+variables [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c d : α}
 
 lemma tsub_le_iff_left : a - b ≤ c ↔ a ≤ b + c :=
 by rw [tsub_le_iff_right, add_comm]
@@ -118,6 +122,83 @@ by rw [tsub_le_iff_left, tsub_le_iff_right]
 lemma tsub_tsub_le : b - (b - a) ≤ a :=
 tsub_le_iff_right.mpr le_add_tsub
 
+section cov
+variable [covariant_class α α (+) (≤)]
+
+lemma tsub_le_tsub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
+tsub_le_iff_left.mpr $ le_add_tsub.trans $ add_le_add_right h _
+
+lemma tsub_le_tsub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
+(tsub_le_tsub_right hab _).trans $ tsub_le_tsub_left hcd _
+
+/-- See `add_tsub_assoc_of_le` for the equality. -/
+lemma add_tsub_le_assoc : a + b - c ≤ a + (b - c) :=
+by { rw [tsub_le_iff_left, add_left_comm], exact add_le_add_left le_add_tsub a }
+
+lemma add_le_add_add_tsub : a + b ≤ (a + c) + (b - c) :=
+by { rw [add_assoc], exact add_le_add_left le_add_tsub a }
+
+lemma le_tsub_add_add : a + b ≤ (a - c) + (b + c) :=
+by { rw [add_comm a, add_comm (a - c)], exact add_le_add_add_tsub }
+
+lemma tsub_le_tsub_add_tsub : a - c ≤ (a - b) + (b - c) :=
+begin
+  rw [tsub_le_iff_left, ← add_assoc, add_right_comm],
+  exact le_add_tsub.trans (add_le_add_right le_add_tsub _),
+end
+
+lemma tsub_tsub_tsub_le_tsub : (c - a) - (c - b) ≤ b - a :=
+begin
+  rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm],
+  exact le_tsub_add.trans (add_le_add_left le_add_tsub _),
+end
+
+lemma tsub_tsub_le_tsub_add {a b c : α} : a - (b - c) ≤ a - b + c :=
+tsub_le_iff_right.2 $ calc
+    a ≤ a - b + b : le_tsub_add
+  ... ≤ a - b + (c + (b - c)) : add_le_add_left le_add_tsub _
+  ... = a - b + c + (b - c) : (add_assoc _ _ _).symm
+
+end cov
+
+/-! #### Lemmas that assume that an element is `add_le_cancellable` -/
+
+namespace add_le_cancellable
+
+protected lemma le_add_tsub_swap (hb : add_le_cancellable b) : a ≤ b + a - b := hb le_add_tsub
+
+protected lemma le_add_tsub (hb : add_le_cancellable b) : a ≤ a + b - b :=
+by { rw add_comm, exact hb.le_add_tsub_swap }
+
+protected lemma le_tsub_of_add_le_left (ha : add_le_cancellable a) (h : a + b ≤ c) : b ≤ c - a :=
+ha $ h.trans le_add_tsub
+
+protected lemma le_tsub_of_add_le_right (hb : add_le_cancellable b) (h : a + b ≤ c) : a ≤ c - b :=
+hb.le_tsub_of_add_le_left $ by rwa add_comm
+
+end add_le_cancellable
+
+/-! ### Lemmas where addition is order-reflecting -/
+
+section contra
+variable [contravariant_class α α (+) (≤)]
+
+lemma le_add_tsub_swap : a ≤ b + a - b := contravariant.add_le_cancellable.le_add_tsub_swap
+
+lemma le_add_tsub' : a ≤ a + b - b := contravariant.add_le_cancellable.le_add_tsub
+
+lemma le_tsub_of_add_le_left (h : a + b ≤ c) : b ≤ c - a :=
+contravariant.add_le_cancellable.le_tsub_of_add_le_left h
+
+lemma le_tsub_of_add_le_right (h : a + b ≤ c) : a ≤ c - b :=
+contravariant.add_le_cancellable.le_tsub_of_add_le_right h
+
+end contra
+
+end add_comm_semigroup
+
+variables [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α}
+
 lemma tsub_nonpos : a - b ≤ 0 ↔ a ≤ b := by rw [tsub_le_iff_left, add_zero]
 
 alias tsub_nonpos ↔ _ tsub_nonpos_of_le
@@ -129,7 +210,9 @@ f.to_add_hom.le_map_tsub hf a b
 
 end preorder
 
-variables [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α}
+/-! ### Partial order -/
+
+variables [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c d : α}
 
 lemma tsub_tsub (b a c : α) : b - a - c = b - (a + c) :=
 begin
@@ -141,12 +224,6 @@ end
 section cov
 variable [covariant_class α α (+) (≤)]
 
-lemma tsub_le_tsub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
-tsub_le_iff_left.mpr $ le_add_tsub.trans $ add_le_add_right h _
-
-lemma tsub_le_tsub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
-(tsub_le_tsub_right hab _).trans $ tsub_le_tsub_left hcd _
-
 lemma tsub_add_eq_tsub_tsub (a b c : α) : a - (b + c) = a - b - c :=
 begin
   refine le_antisymm (tsub_le_iff_left.mpr _)
@@ -158,41 +235,14 @@ end
 lemma tsub_add_eq_tsub_tsub_swap (a b c : α) : a - (b + c) = a - c - b :=
 by { rw [add_comm], apply tsub_add_eq_tsub_tsub }
 
-lemma add_le_add_add_tsub : a + b ≤ (a + c) + (b - c) :=
-by { rw [add_assoc], exact add_le_add_left le_add_tsub a }
-
 lemma tsub_right_comm : a - b - c = a - c - b :=
 by simp_rw [← tsub_add_eq_tsub_tsub, add_comm]
 
-/-- See `add_tsub_assoc_of_le` for the equality. -/
-lemma add_tsub_le_assoc : a + b - c ≤ a + (b - c) :=
-by { rw [tsub_le_iff_left, add_left_comm], exact add_le_add_left le_add_tsub a }
-
-lemma le_tsub_add_add : a + b ≤ (a - c) + (b + c) :=
-by { rw [add_comm a, add_comm (a - c)], exact add_le_add_add_tsub }
-
-lemma tsub_le_tsub_add_tsub : a - c ≤ (a - b) + (b - c) :=
-begin
-  rw [tsub_le_iff_left, ← add_assoc, add_right_comm],
-  refine le_add_tsub.trans (add_le_add_right le_add_tsub _),
-end
-
-lemma tsub_tsub_tsub_le_tsub : (c - a) - (c - b) ≤ b - a :=
-begin
-  rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm],
-  refine le_tsub_add.trans (add_le_add_left le_add_tsub _),
-end
-
 end cov
 
 /-! ### Lemmas that assume that an element is `add_le_cancellable`. -/
-namespace add_le_cancellable
-
-protected lemma le_add_tsub_swap (hb : add_le_cancellable b) : a ≤ b + a - b :=
-hb le_add_tsub
 
-protected lemma le_add_tsub (hb : add_le_cancellable b) : a ≤ a + b - b :=
-by { rw [add_comm], exact hb.le_add_tsub_swap }
+namespace add_le_cancellable
 
 protected lemma tsub_eq_of_eq_add (hb : add_le_cancellable b) (h : a = c + b) : a - b = c :=
 le_antisymm (tsub_le_iff_right.mpr h.le) $
@@ -212,12 +262,6 @@ hb.tsub_eq_of_eq_add $ by rw [add_comm]
 protected lemma add_tsub_cancel_left (ha : add_le_cancellable a) : a + b - a = b :=
 ha.tsub_eq_of_eq_add $ add_comm a b
 
-protected lemma le_tsub_of_add_le_left (ha : add_le_cancellable a) (h : a + b ≤ c) : b ≤ c - a :=
-ha $ h.trans le_add_tsub
-
-protected lemma le_tsub_of_add_le_right (hb : add_le_cancellable b) (h : a + b ≤ c) : a ≤ c - b :=
-hb.le_tsub_of_add_le_left $ by rwa [add_comm]
-
 protected lemma lt_add_of_tsub_lt_left (hb : add_le_cancellable b) (h : a - b < c) : a < b + c :=
 begin
   rw [lt_iff_le_and_ne, ← tsub_le_iff_left],
@@ -236,17 +280,11 @@ end
 
 end add_le_cancellable
 
-/-! ### Lemmas where addition is order-reflecting. -/
+/-! #### Lemmas where addition is order-reflecting. -/
 
 section contra
 variable [contravariant_class α α (+) (≤)]
 
-lemma le_add_tsub_swap : a ≤ b + a - b :=
-contravariant.add_le_cancellable.le_add_tsub_swap
-
-lemma le_add_tsub' : a ≤ a + b - b :=
-contravariant.add_le_cancellable.le_add_tsub
-
 lemma tsub_eq_of_eq_add (h : a = c + b) : a - b = c :=
 contravariant.add_le_cancellable.tsub_eq_of_eq_add h
 
@@ -264,12 +302,6 @@ contravariant.add_le_cancellable.add_tsub_cancel_right
 lemma add_tsub_cancel_left (a b : α) : a + b - a = b :=
 contravariant.add_le_cancellable.add_tsub_cancel_left
 
-lemma le_tsub_of_add_le_left (h : a + b ≤ c) : b ≤ c - a :=
-contravariant.add_le_cancellable.le_tsub_of_add_le_left h
-
-lemma le_tsub_of_add_le_right (h : a + b ≤ c) : a ≤ c - b :=
-contravariant.add_le_cancellable.le_tsub_of_add_le_right h
-
 lemma lt_add_of_tsub_lt_left (h : a - b < c) : a < b + c :=
 contravariant.add_le_cancellable.lt_add_of_tsub_lt_left h
 
@@ -300,7 +332,7 @@ end ordered_add_comm_monoid
 
 /-! ### Lemmas in a linearly ordered monoid. -/
 section linear_order
-variables {a b c d : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α]
+variables {a b c d : α} [linear_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α]
 
 /-- See `lt_of_tsub_lt_tsub_right_of_le` for a weaker statement in a partial order. -/
 lemma lt_of_tsub_lt_tsub_right (h : a - c < b - c) : a < b :=