a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
let t := pellZd_add a1 n (m - n)
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
rw [add_tsub_cancel_of_le h] at t
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]