proposition: Theorem pow_add : forall (e : R) (n m : nat), (e ^ (n + m))%R = (e ^ n * e ^ m)%R.
proof: Proof. intros e n; elim n; simpl in |- *; auto with real. intros n0 H' m; rewrite H'; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz