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