proposition: Theorem Rlt_pow_R1 : forall (e : R) (n : nat), (1 < e)%R -> 0 < n -> (1 < e ^ n)%R.
proof: Proof. intros e n; elim n; simpl in |- *; auto with real. intros H' H'0; contradict H'0; auto with arith. intros n0; case n0. simpl in |- *; rewrite Rmult_1_r; auto. intros n1 H' H'0 H'1. replace 1%R with (1 * 1)%R; auto with real. apply Rlt_trans with (r2 := (e * 1)%R); auto with real. apply Rmult_lt_compat_l; auto with real. apply Rlt_trans with (r2 := 1%R); auto with real. apply H'; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz