no goals
β : Type ?u.267249
A : Type ?u.267252
G : Type ?u.267255
M : Type ?u.267258
R : Type u_1
inst✝ : LinearOrderedRing R
x✝ y✝ x y : R
⊢ x ^ 2 = y ^ 2 ↔ abs x = abs y
simp only [le_antisymm_iff, sq_le_sq]