simp only [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq] at this
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : r 1 * sr 0 = sr 0 * r 1
⊢ False
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False