no goals
β : Type ?u.268169
A : Type ?u.268172
G : Type ?u.268175
M : Type ?u.268178
R : Type u_1
inst✝ : LinearOrderedRing R
x✝ y x : R
⊢ x ^ 2 ≤ 1 ↔ abs x ≤ 1
simpa only [one_pow, abs_one] using @sq_le_sq _ _ x 1