proposition: Lemma inj_zexp : forall (n : nat) (a : Z), ZExp a (Z_of_nat n) = Exp a n.
proof: Proof. simple induction n. simpl in |- *. reflexivity. intros m IH. intros. simpl in |- *. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. simpl in |- *. reflexivity. Qed.
imports: ZArith lemmas natZ