case intro
R : Type u_1
S : Type ?u.68228
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - ↑C a * dickson k a (2 + n - 2)
R : Type u_1
S : Type ?u.68228
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
⊢ dickson k a n = X * dickson k a (n - 1) - ↑C a * dickson k a (n - 2)
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
case intro
R : Type u_1
S : Type ?u.68228
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - ↑C a * dickson k a (n + 2 - 2)
case intro
R : Type u_1
S : Type ?u.68228
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - ↑C a * dickson k a (2 + n - 2)
rw [add_comm]
no goals
case intro
R : Type u_1
S : Type ?u.68228
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - ↑C a * dickson k a (n + 2 - 2)
exact dickson_add_two k a n