proposition: Lemma log2_spec n : 0<n -> 2^(log2 n) <= n < 2^(S (log2 n)).
proof: Proof. intros. set (s:=log2 n). replace n with (pred n + 1). - apply log2_iter_spec; auto. - rewrite add_1_r. apply succ_pred. now apply neq_sym, lt_neq. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass