feat(algebra/group_power/basic): add abs_add_eq_add_abs_iff (#6593)

I've added
```
lemma abs_add_eq_add_abs_iff {α : Type*} [linear_ordered_add_comm_group α]  (a b : α) :
  abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
```
from `lean-liquid`. For some reasons I am not able to use `wlog hle : a ≤ b using [a b, b a]` at the beginning of the proof, Lean says `unknown identifier 'wlog'` and if I try to import `tactic.wlog` I have tons of errors.

Author: riccardobrasca

src/algebra/group_power/lemmas.lean

@@ -182,6 +182,57 @@ calc n •ℤ a = n •ℤ a + 0 : (add_zero _).symm
   ... < n •ℤ a + (m - n) •ℤ a : add_lt_add_left (gsmul_pos ha (sub_pos.mpr h)) _
   ... = m •ℤ a : by { rw [← add_gsmul], simp }
 
+lemma abs_nsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℕ) (a : α) :
+  abs (n •ℕ a) = n •ℕ abs a :=
+begin
+  cases le_total a 0 with hneg hpos,
+  { rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg],
+    exact nsmul_nonneg (neg_nonneg.mpr hneg) n },
+  { rw [abs_of_nonneg hpos, abs_of_nonneg],
+    exact nsmul_nonneg hpos n }
+end
+
+lemma abs_gsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℤ) (a : α) :
+  abs (n •ℤ a) = (abs n) •ℤ abs a :=
+begin
+  by_cases n0 : 0 ≤ n,
+  { lift n to ℕ using n0,
+    simp only [abs_nsmul, coe_nat_abs, gsmul_coe_nat] },
+  { lift (- n) to ℕ using int.le_of_lt (neg_pos.mpr (not_le.mp n0)) with m h,
+    rw [← abs_neg (n •ℤ a), ← neg_gsmul, ← abs_neg n, ← h],
+    convert abs_nsmul m _,
+    simp only [coe_nat_abs, gsmul_coe_nat] },
+end
+
+lemma abs_add_eq_add_abs_le {α : Type*} [linear_ordered_add_comm_group α] {a b : α} (hle : a ≤ b) :
+  abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+begin
+  by_cases a0 : 0 ≤ a; by_cases b0 : 0 ≤ b,
+  { simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0] },
+  { exact (lt_irrefl (0 : α) (a0.trans_lt (hle.trans_lt (not_le.mp b0)))).elim },
+  any_goals { simp [(not_le.mp a0).le, (not_le.mp b0).le, abs_of_nonpos, add_nonpos, add_comm] },
+  obtain F := (not_le.mp a0),
+  have : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) =
+    abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0),
+  { simp [a0, b0, abs_of_neg, abs_of_nonneg, F, F.le] },
+  refine this.mp ⟨λ h, _, λ h, by simp only [le_antisymm h b0, abs_of_neg F, add_zero]⟩,
+  by_cases ba : a + b ≤ 0,
+  { refine le_of_eq (eq_zero_of_neg_eq _),
+    rwa [abs_of_nonpos ba, neg_add_rev, add_comm, add_right_inj] at h },
+  { refine (lt_irrefl (0 : α) _).elim,
+    rw [abs_of_pos (not_le.mp ba), add_left_inj] at h,
+    rwa eq_zero_of_neg_eq h.symm at F }
+end
+
+lemma abs_add_eq_add_abs_iff {α : Type*} [linear_ordered_add_comm_group α] (a b : α) :
+  abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+begin
+  by_cases ab : a ≤ b,
+  { exact abs_add_eq_add_abs_le ab },
+  { rw [add_comm a, add_comm (abs _), abs_add_eq_add_abs_le ((not_le.mp ab).le), and.comm,
+    @and.comm (b ≤ 0 ) _] }
+end
+
 end ordered_add_comm_group
 
 section linear_ordered_add_comm_group