proposition: Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x).
proof: Proof. intros x. rewrite Ndigits_fold, digits_fold. destr_t x as (n,x). apply ZnZ.spec_zdigits. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen