proposition: Lemma power_mult : forall (a : M) (n p : nat), power a (p * n) = power (power a n) p.
proof: Proof. simple induction p; simpl in |- *. auto with arith. intros n0 H. rewrite power_plus. elim H; auto with arith. Qed.
imports: Arith Constants