proposition: Theorem spec_of_N: forall x, [of_N x] = Z.of_N x.
proof: Proof. intros x; case x. simpl of_N. exact spec_0. intros p; exact (spec_of_pos p). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen