proposition: Lemma exp_correct m n: [exp_num m n] = Zpower_nat [m] n.
proof: Proof. induction n as [ | n Hrec]; unfold exp_num; fold exp_num. nrom; nrom; unfold Zpower_nat; simpl; auto. change (S n) with (1 + n)%nat; rewrite Zpower_nat_is_exp. rewrite prod_correct, Hrec; change (Zpower_nat [m] 1) with ([m] * 1)%Z. ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63