log2n.v

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
  helper n n.