proposition: Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y].
proof: Proof. intros. unfold pow, to_N. now rewrite spec_pow_N, Z2N.id by apply spec_pos. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen