proposition: Lemma log_double : forall n, n > 0 -> log(2*n) = 1 + log n.
proof: Proof. Proof using. introv Pos. rewrite fix_log. unfold Log. case_if*. fequals. rewrite~ Nat.div2_double. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat