proposition: Theorem spec_pos: forall x, 0 <= [x].
proof: Proof. intros x. destr_t x as (n,x). now case (ZnZ.spec_to_Z x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen