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