proposition: Lemma exp_mult : forall (a : Z) (n m : nat), Exp a (n * m) = Exp (Exp a n) m.
proof: Proof. simple induction n. simpl in |- *. intro. rewrite exp_1. reflexivity. intros m IH. simpl in |- *. intros. rewrite exp_plus. rewrite exp_abn. rewrite IH. reflexivity. Qed.
imports: ZArith lemmas natZ