proposition: Theorem spec_head0: forall x, 0 < [x] -> 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x).
proof: Proof. intros x. rewrite pow2_pos_minus_1 by (red; auto). rewrite head0_fold, digits_fold. destr_t x as (n,x). exact (ZnZ.spec_head0 x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen