no goals
β : Type ?u.260389
A : Type ?u.260392
G : Type ?u.260395
M : Type ?u.260398
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).le_iff_le (abs_nonneg x) (abs_nonneg y)