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