proposition: Lemma Z2Nat_pow (a b : Z) : 0 <= a -> 0 <= b -> Z.to_nat (a ^ b) = (Z.to_nat a ^ Z.to_nat b)%nat.
proof: Proof. intros pa pb. rewrite <-(Z2Nat.id a) at 1; auto. rewrite <-(Z2Nat.id b) at 1; auto. rewrite <-Nat2Z_pow. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)