Q : Type ?u.78946
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b
Q : Type ?u.78946
inst✝ : Quandle Q
n : ℕ
a : ZMod n
⊢ Function.Involutive (dihedralAct n a)
intro b
Q : Type ?u.78946
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b
Q : Type ?u.78946
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b
dsimp only [dihedralAct]
no goals
Q : Type ?u.78946
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b
simp