proposition: Lemma zexp_plus : forall a n m : Z, (0 <= n)%Z -> (0 <= m)%Z -> ZExp a (n + m) = (ZExp a n * ZExp a m)%Z.
proof: Proof. intros. rewrite expzexp. rewrite expzexp. rewrite expzexp. rewrite abs_plus_pos. apply exp_plus. assumption. assumption. Qed.
imports: ZArith lemmas natZ