proposition: Lemma inj_pow: forall n m : Z, (0 <= n)%Z -> (0 <= m)%Z -> Z.to_nat (n ^ m) = Z.to_nat n ^ Z.to_nat m.
proof: Proof. intros. pose proof (Nat2Z.inj_pow (Z.to_nat n) (Z.to_nat m)) as P. rewrite? Z2Nat.id in P by assumption. rewrite <- P. apply Nat2Z.id. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.micromega.Lia