no goals
R : Type u_1
S : Type ?u.123904
M : Type ?u.123907
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]