9-42.v

Require Import Arith.
Require Import Omega.
Require Import Recdef.

Function log(n:nat) {wf lt n} :=
  if le_lt_dec n 1 then
    0
  else
    S (log (Div2.div2 n)).
Proof.
intros.
apply Div2.lt_div2.
omega.
apply well_founded_ltof.
Qed.