proposition: Lemma power_power : forall x a b : nat, power (power x a) b = power x (a * b).
proof: Proof. simple induction b; simpl in |- *; auto. rewrite Nat.mul_comm; simpl in |- *; auto. intros n H'; rewrite Nat.mul_comm with (m := S n); simpl in |- *; rewrite (Nat.mul_comm n); rewrite H'; apply power_mult. Qed.
imports: Coq(Arith ArithRing)