proposition: Lemma exp_plus : forall (a : Z) (n m : nat), Exp a (n + m) = (Exp a n * Exp a m)%Z.
proof: Proof. simple induction n. simpl in |- *. intros. elim (Exp a m). reflexivity. reflexivity. reflexivity. intros n1 IH. simpl in |- *. intros. rewrite (IH m). apply Zmult_assoc. Qed.
imports: ZArith lemmas natZ