feat(algebra/group_power/basic): abs_lt_abs_of_sqr_lt_sqr (#6277)

These lemmas are (almost) the converses of some of the lemmas I added in #5933.

src/algebra/group_power/basic.lean

@@ -640,10 +640,10 @@ pow_bit0_pos h 1
 
 variables {x y : R}
 
-@[simp] theorem sqr_abs : abs x ^ 2 = x ^ 2 :=
+@[simp] theorem sqr_abs (x : R) : abs x ^ 2 = x ^ 2 :=
 by simpa only [pow_two] using abs_mul_abs_self x
 
-theorem abs_sqr : abs (x ^ 2) = x ^ 2 :=
+theorem abs_sqr (x : R) : abs (x ^ 2) = x ^ 2 :=
 by simpa only [pow_two] using abs_mul_self x
 
 theorem sqr_lt_sqr (h : abs x < y) : x ^ 2 < y ^ 2 :=
@@ -658,6 +658,30 @@ by simpa only [sqr_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
 theorem sqr_le_sqr' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
 sqr_le_sqr (abs_le.mpr ⟨h1, h2⟩)
 
+theorem abs_lt_abs_of_sqr_lt_sqr (h : x^2 < y^2) : abs x < abs y :=
+lt_of_pow_lt_pow 2 (abs_nonneg y) $ by rwa [← sqr_abs x, ← sqr_abs y] at h
+
+theorem abs_lt_of_sqr_lt_sqr (h : x^2 < y^2) (hy : 0 ≤ y) : abs x < y :=
+begin
+  rw [← abs_of_nonneg hy],
+  exact abs_lt_abs_of_sqr_lt_sqr h,
+end
+
+theorem abs_lt_of_sqr_lt_sqr' (h : x^2 < y^2) (hy : 0 ≤ y) : -y < x ∧ x < y :=
+abs_lt.mp $ abs_lt_of_sqr_lt_sqr h hy
+
+theorem abs_le_abs_of_sqr_le_sqr (h : x^2 ≤ y^2) : abs x ≤ abs y :=
+le_of_pow_le_pow 2 (abs_nonneg y) (1:ℕ).succ_pos $ by rwa [← sqr_abs x, ← sqr_abs y] at h
+
+theorem abs_le_of_sqr_le_sqr (h : x^2 ≤ y^2) (hy : 0 ≤ y) : abs x ≤ y :=
+begin
+  rw [← abs_of_nonneg hy],
+  exact abs_le_abs_of_sqr_le_sqr h,
+end
+
+theorem abs_le_of_sqr_le_sqr' (h : x^2 ≤ y^2) (hy : 0 ≤ y) : -y ≤ x ∧ x ≤ y :=
+abs_le.mp $ abs_le_of_sqr_le_sqr h hy
+
 end linear_ordered_ring
 
 @[simp] lemma eq_of_pow_two_eq_pow_two [linear_ordered_comm_ring R]