no goals
β : Type ?u.257384
A : Type ?u.257387
G : Type ?u.257390
M : Type ?u.257393
R : Type u_1
inst✝ : LinearOrderedRing R
x y : R
⊢ x ^ 2 < y ^ 2 ↔ abs x < abs y
simpa only [sq_abs] using
  (@strictMonoOn_pow R _ _ two_pos).lt_iff_lt (abs_nonneg x) (abs_nonneg y)