proposition: Lemma fix_log : forall n, log n = Log log n.
proof: Proof. Proof using. applys~ (FixFun_fix (@lt nat _)). introv H. unfolds. case_if~. fequals. apply H. apply* div2_lt. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat