proposition: Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
proof: Proof. intros x; case x; clear x; intros x. exact (NN.spec_succ x). simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl. intros HH; rewrite <- HH; rewrite NN.spec_1; ring. intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith. generalize (NN.spec_pos x); auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig