R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * X - 1 = X * X - (1 - X ^ 2) * 1
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (0 + 2) = X * T R (0 + 1) - (1 - X ^ 2) * U R 0
simp only [T, U]
no goals
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * X - 1 = X * X - (1 - X ^ 2) * 1
ring
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X * X - 1) - X = X * (2 * X * X - 1) - (1 - X ^ 2) * (2 * X)
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (1 + 2) = X * T R (1 + 1) - (1 - X ^ 2) * U R 1
simp only [T, U]
no goals
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X * X - 1) - X = X * (2 * X * X - 1) - (1 - X ^ 2) * (2 * X)
ring
no goals
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * T R (n + 2 + 1) - T R (n + 2) =
    2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n)
simp only [T_eq_X_mul_T_sub_pol_U]
no goals
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n) =
    X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n)
ring
no goals
R : Type u_1
S : Type ?u.22740
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n) =
    X * T R (n + 2 + 1) - (1 - X ^ 2) * U R (n + 2)
rw [T_add_two _ (n + 1), U_add_two]