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