proposition: Lemma zexp_mult : forall a n m : Z, (0 <= n)%Z -> (0 <= m)%Z -> ZExp a (n * m) = ZExp (ZExp a n) m.
proof: Proof. intros. rewrite expzexp. rewrite expzexp. rewrite expzexp. rewrite abs_mult. apply exp_mult. Qed.
imports: ZArith lemmas natZ