proposition: Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y.
proof: Proof. intros. unfold pow. destruct (to_Z y); simpl. apply NN.spec_1. apply spec_pow_pos. apply NN.spec_0. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig