lean_workbook_plus_43100
ProvedDetermine the value of modulo 3.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43100 (x : ℕ → ℕ) (h : x 0 = 1 ∧ ∀ n, x (n + 1) = x n + x (n + 2)) : x 2004 % 3 = 1 := by sorry
Source