Fibonacci function by kdxu

module Theorem where
open import Data.Nat
open import Definitions
fib : ℕ → ℕ
fib (suc (suc c)) = fib (suc c) + fib c
fib c = 1
fib-is-FibFunc : FibFunc fib
fib-is-FibFunc zero = Fib0
fib-is-FibFunc (suc zero) = Fib1
fib-is-FibFunc (suc (suc n)) = FibN (fib-is-FibFunc (suc n)) (fib-is-FibFunc n)