proposition: Theorem Rlt_pow : forall (e : R) (n m : nat), (1 < e)%R -> n < m -> (e ^ n < e ^ m)%R.
proof: Proof. intros e n m H' H'0; replace m with (m - n + n). rewrite pow_add. pattern (e ^ n)%R at 1 in |- *; replace (e ^ n)%R with (1 * e ^ n)%R; auto with real. apply Rminus_lt. repeat rewrite (fun x : R => Rmult_comm x (e ^ n)); rewrite <- Rmult_minus_distr_l. replace 0%R with (e ^ n * 0)%R; auto with real. apply Rmult_lt_compat_l; auto with real. apply pow_lt; auto with real. apply Rlt_trans with (r2 := 1%R); auto with real. apply Rlt_minus; auto with real. apply Rlt_pow_R1; auto with arith. apply Nat.add_lt_mono_l with (p := n); auto with arith. rewrite Nat.add_0_r, Nat.add_comm, Nat.sub_add; auto with arith. rewrite Nat.add_comm; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz