no goals
β : Type ?u.263157
A : Type ?u.263160
G : Type ?u.263163
M : Type ?u.263166
R : Type u_1
inst✝ : LinearOrderedRing R
x y : R
h : x ^ 2 < y ^ 2
hy : 0 ≤ y
⊢ abs x < y
rwa [← abs_of_nonneg hy, ← sq_lt_sq]