Fixpoint rec_fib (m : nat) (a : nat) (b : nat) : nat :=
  match m with
    | 0 => a
    | S k => rec_fib k b (a + b)
  end.

Definition fib (n : nat) : nat :=
  rec_fib n 0 1 .