proposition: Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y.
proof: Proof. unfold sub, to_Z; intros [x | x] [y | y]; try (rewrite NN.spec_add; auto with zarith); rewrite NN.spec_compare; case Z.compare_spec; unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; lia. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig