no goals
R : Type u_1
S : Type ?u.255623
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ comp (dickson 1 1 m) (dickson 1 1 n) = comp (dickson 1 1 n) (dickson 1 1 m)
rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]