rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_ofNat_of_lt hn] at this
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : 2 = 0
⊢ False