Nat.fib_greatestFib_le
theorem Nat.fib_greatestFib_le : ∀ (n : ℕ), n.greatestFib.fib ≤ n
The theorem `Nat.fib_greatestFib_le` states that for all natural numbers `n`, the Fibonacci number at the greatest index less than or equal to `n` is itself less than or equal to `n`. In other words, for any natural number `n`, if you find the largest index `k` such that the `k`-th Fibonacci number is less than or equal to `n`, then the `k`-th Fibonacci number is indeed less than or equal to `n`.
More concisely: For all natural numbers n, the largest Fibonacci number less than or equal to n is less than or equal to n.
|
Nat.zeckendorf_succ
theorem Nat.zeckendorf_succ :
∀ (n : ℕ), (n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - (n + 1).greatestFib.fib).zeckendorf
The theorem `Nat.zeckendorf_succ` states that for any natural number `n`, the Zeckendorf representation of `n + 1` is a list that starts with the greatest index of a Fibonacci number less than or equal to `n + 1`, followed by the Zeckendorf representation of `n + 1 - fib(greatestFib(n + 1))`. This represents that the Zeckendorf representation of `n + 1` is constructed by adding the largest possible Fibonacci number (without exceeding `n + 1`), then recursively doing the same for the remainder after subtracting this Fibonacci number.
More concisely: The Zeckendorf representation of `n + 1` is obtained by appending the index of the largest Fibonacci number less than or equal to `n + 1` to the Zeckendorf representation of `n + 1 - Fib(greatest Fibonacci number <= n + 1)`.
|