proposition: Lemma log_grows : forall n m, m <= n -> log m <= log n.
proof: Proof. Proof using. induction n using peano_induction. introv Le. do 2 rewrite fix_log. unfolds Log. (do 2 case_if); autos*. forwards: H (Nat.div2 n) (Nat.div2 m). apply* div2_lt. apply~ div2_grows. math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat