anton-trunov

Definition log2 n :=
  let helper :=
      (fix log2_helper n dummy :=
         match dummy with
         | 0 => 0
         | S d' => match n with
                  | 0 | 1 => 0
                  | n => S (log2_helper (Nat.div2 n) d')
                  end
         end) in

anton-trunov

Require Import Arith.

Fixpoint fib_v1 (n : nat) : nat :=
  match n with
  | 0 => O
  | S n' => match n' with
            | O => 1
            | S n'' => (fib_v1 n') + (fib_v1 n'')
            end
  end.