Fibonacci function by phi16_

module Theorem where

open import Data.Nat
open import Definitions

fib : ℕ → ℕ
fib 0 = 1
fib 1 = 1
fib (suc (suc x)) = fib (suc x) + fib x

fib-is-FibFunc : FibFunc fib
fib-is-FibFunc 0 = Fib0
fib-is-FibFunc 1 = Fib1
fib-is-FibFunc (suc (suc n)) = FibN (fib-is-FibFunc (suc n)) (fib-is-FibFunc n)