α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution { order := 2, coeffs := ![1, 1] } fun x => ↑(Nat.fib x)
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => ↑(Nat.fib x)
rw [fibRec]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    Finset.sum Finset.univ fun i =>
      LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i * (fun x => ↑(Nat.fib x)) (n + ↑i)
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution { order := 2, coeffs := ![1, 1] } fun x => ↑(Nat.fib x)
intro n
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    Finset.sum Finset.univ fun i =>
      LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i * (fun x => ↑(Nat.fib x)) (n + ↑i)
simp only
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
rw [Nat.fib_add_two, add_comm]
no goals
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']