proposition: Lemma inj_pow: forall n m : nat, Z.of_nat (n ^ m) = (Z.of_nat n ^ Z.of_nat m)%Z.
proof: Proof. intros. induction m. - reflexivity. - rewrite Nat2Z.inj_succ. rewrite Z.pow_succ_r by (apply Nat2Z.is_nonneg). rewrite <- IHm. rewrite <- Nat2Z.inj_mul. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.micromega.Lia