Fibonacci function by kiritex

module Theorem where

  open import Data.Nat
  open import Definitions

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

  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)