no goals
β : Type ?u.269074
A : Type ?u.269077
G : Type ?u.269080
M : Type ?u.269083
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_lt_sq _ _ x 1