proposition: Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x).
proof: Proof. intros x. rewrite digits_fold. destr_t x as (n,x). exact (ZnZ.spec_to_Z x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen