no goals
β : Type ?u.269979
A : Type ?u.269982
G : Type ?u.269985
M : Type ?u.269988
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_le_sq _ _ 1 x