chore(algebra/ordered_ring): add a few simp lemmas (#5749)

* fix misleading names `neg_lt_iff_add_nonneg` → `neg_lt_iff_pos_add`,
  `neg_lt_iff_add_nonneg'` → `neg_lt_iff_pos_add'`;
* add `@[simp]` to `abs_mul_abs_self` and `abs_mul_self`;
* add lemmas `neg_le_self_iff`, `neg_lt_self_iff`, `le_neg_self_iff`,
  `lt_neg_self_iff`, `abs_eq_self`, `abs_eq_neg_self`.

src/algebra/ordered_group.lean

@@ -282,11 +282,11 @@ lemma inv_le_iff_one_le_mul : a⁻¹ ≤ b ↔ 1 ≤ b * a :=
 lemma inv_le_iff_one_le_mul' : a⁻¹ ≤ b ↔ 1 ≤ a * b :=
 (mul_le_mul_iff_left a).symm.trans $ by rw mul_inv_self
 
-@[to_additive neg_lt_iff_add_nonneg]
+@[to_additive]
 lemma inv_lt_iff_one_lt_mul : a⁻¹ < b ↔ 1 < b * a :=
 (mul_lt_mul_iff_right a).symm.trans $ by rw inv_mul_self
 
-@[to_additive neg_lt_iff_add_nonneg']
+@[to_additive]
 lemma inv_lt_iff_one_lt_mul' : a⁻¹ < b ↔ 1 < a * b :=
 (mul_lt_mul_iff_left a).symm.trans $ by rw mul_inv_self
 

src/algebra/ordered_ring.lean

@@ -629,10 +629,10 @@ end
 /-- `abs` as a `monoid_with_zero_hom`. -/
 def abs_hom : monoid_with_zero_hom α α := ⟨abs, abs_zero, abs_one, abs_mul⟩
 
-lemma abs_mul_abs_self (a : α) : abs a * abs a = a * a :=
+@[simp] lemma abs_mul_abs_self (a : α) : abs a * abs a = a * a :=
 abs_by_cases (λ x, x * x = a * a) rfl (neg_mul_neg a a)
 
-lemma abs_mul_self (a : α) : abs (a * a) = a * a :=
+@[simp] lemma abs_mul_self (a : α) : abs (a * a) = a * a :=
 by rw [abs_mul, abs_mul_abs_self]
 
 lemma mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
@@ -652,6 +652,26 @@ by rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff, neg_nonneg, neg_nonpo
 lemma mul_self_nonneg (a : α) : 0 ≤ a * a :=
 abs_mul_self a ▸ abs_nonneg _
 
+@[simp] lemma neg_le_self_iff : -a ≤ a ↔ 0 ≤ a :=
+by simp [neg_le_iff_add_nonneg, ← two_mul, mul_nonneg_iff, zero_le_one, (@zero_lt_two α _ _).not_le]
+
+@[simp] lemma neg_lt_self_iff : -a < a ↔ 0 < a :=
+by simp [neg_lt_iff_pos_add, ← two_mul, mul_pos_iff, zero_lt_one, (@zero_lt_two α _ _).not_lt]
+
+@[simp] lemma le_neg_self_iff : a ≤ -a ↔ a ≤ 0 :=
+calc a ≤ -a ↔ -(-a) ≤ -a : by rw neg_neg
+... ↔ 0 ≤ -a : neg_le_self_iff
+... ↔ a ≤ 0 : neg_nonneg
+
+@[simp] lemma lt_neg_self_iff : a < -a ↔ a < 0 :=
+calc a < -a ↔ -(-a) < -a : by rw neg_neg
+... ↔ 0 < -a : neg_lt_self_iff
+... ↔ a < 0 : neg_pos
+
+@[simp] lemma abs_eq_self : abs a = a ↔ 0 ≤ a := by simp [abs]
+
+@[simp] lemma abs_eq_neg_self : abs a = -a ↔ a ≤ 0 := by simp [abs]
+
 lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
 have nhc : 0 ≤ -c, from neg_nonneg_of_nonpos hc,
 have h2 : -(c * b) < -(c * a), from neg_lt_neg h,
@@ -661,11 +681,7 @@ have h3 : (-c) * b < (-c) * a, from calc
           ... = (-c) * a     : by rewrite neg_mul_eq_neg_mul,
 lt_of_mul_lt_mul_left h3 nhc
 
-lemma neg_one_lt_zero : -1 < (0:α) :=
-begin
-  have this := neg_lt_neg (@zero_lt_one α _ _),
-  rwa neg_zero at this
-end
+lemma neg_one_lt_zero : -1 < (0:α) := neg_lt_zero.2 zero_lt_one
 
 lemma le_of_mul_le_of_one_le {a b c : α} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) :
   a ≤ b :=