proposition: Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x].
proof: Proof. intros. destruct (Z_lt_ge_dec 0 [x]). symmetry. apply Z.log2_unique. apply spec_pos. apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith. rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith. generalize (spec_pos x); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen