proposition: Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1.
proof: Proof. unfold pred, to_Z, minus_one; intros [x | x]; try (rewrite NN.spec_succ; ring). rewrite NN.spec_compare; case Z.compare_spec; rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred; generalize (NN.spec_pos x); lia. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig