proposition: Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)).
proof: Proof. intros x. rewrite digits_fold. unfold level. destr_t x as (n,x). reflexivity. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen