no goals
β : Type ?u.270901
A : Type ?u.270904
G : Type ?u.270907
M : Type ?u.270910
R : Type u_1
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ 1 < x ^ 2 ↔ 1 < abs x
simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 x