no goals
β : Type ?u.265331
A : Type ?u.265334
G : Type ?u.265337
M : Type ?u.265340
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_le_sq]