proposition: Lemma log_compute : log 256 = 8.
proof: Proof. Proof using. rewrite (@fix_log many_steps). dup. { reflexivity. } { applys eq_trans. unfold Log; simpl. eauto. eauto. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat