proposition: Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.
proof: Proof. destruct n; simpl. apply spec_1. apply spec_pow_pos. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen