no goals
R : Type u_1
S : Type ?u.134487
M : Type ?u.134490
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a✝ b✝ : R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]