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