fix(algebra/ordered_group): use add_neg in autogenerated lemma name (…

…#4580)

Explicitly add `sub_le_sub_iff` with `a - b`.

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -133,7 +133,7 @@ lemma div_le_div' (a b c d : α) (hb : b ≠ 0) (hd : d ≠ 0) :
 begin
   by_cases ha : a = 0, { simp [ha] },
   by_cases hc : c = 0, { simp [inv_ne_zero hb, hc, hd], },
-  exact (div_le_div_iff' (units.mk0 a ha) (units.mk0 b hb) (units.mk0 c hc) (units.mk0 d hd)),
+  exact @div_le_div_iff' _ _ (units.mk0 a ha) (units.mk0 b hb) (units.mk0 c hc) (units.mk0 d hd)
 end
 
 lemma ne_zero_of_lt (h : b < a) : a ≠ 0 :=

src/algebra/ordered_group.lean

@@ -1208,8 +1208,8 @@ by rwa inv_mul_cancel_left at this
 lemma inv_mul_lt_iff_lt_mul_right : c⁻¹ * a < b ↔ a < b * c :=
 by rw [inv_mul_lt_iff_lt_mul, mul_comm]
 
-@[to_additive sub_le_sub_iff]
-lemma div_le_div_iff' (a b c d : α) : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
+@[to_additive add_neg_le_add_neg_iff]
+lemma div_le_div_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
 begin
   split ; intro h,
   have := mul_le_mul_right' (mul_le_mul_right' h b) d,
@@ -1439,6 +1439,8 @@ calc
     ... < a + 0  : add_lt_add_left (neg_neg_of_pos h) _
     ... = a      : by rw add_zero
 
+lemma sub_le_sub_iff : a - b ≤ c - d ↔ a + d ≤ c + b := add_neg_le_add_neg_iff
+
 @[simp]
 lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
 (add_le_add_iff_left _).trans neg_le_neg_iff