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