Fibonacci function by Lost_dog_

module Theorem where

open import Data.Nat
open import Definitions

open import Data.Product
open import Induction.Nat

fib : ℕ → ℕ
fib = cRec _ f
  where
  f : ∀ k → CRec _ k → ℕ
  f (suc (suc k)) (p , q , _) = p + q
  f _ _ = 1

fib-is-FibFunc : ∀ n →  Fib n (fib n)
fib-is-FibFunc = cRec _ f
  where
  f : ∀ k → CRec _ k → Fib k (fib k)
  f 0 _ = Fib0
  f 1 _ = Fib1
  f (suc (suc k)) (p , q , _) = FibN p q