proposition: Lemma Zpower_nat_Z (z : Z) (n : nat) : Zpower_nat z n = z ^ (Z.of_nat n).
proof: Proof. induction n. - trivial. - rewrite Zpower_nat_succ_r, Nat2Z.inj_succ, Z.pow_succ_r. + now f_equal. + apply Nat2Z.is_nonneg. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def