proposition: Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
proof: Proof. intros x n m H' H'0; replace m with (m - n + n)%nat. - rewrite pow_add. pattern (x ^ n) at 1; replace (x ^ n) with (1 * x ^ n); auto with real. apply Rminus_lt. repeat rewrite (fun y:R => Rmult_comm y (x ^ n)); rewrite <- Rmult_minus_distr_l. replace 0 with (x ^ n * 0); auto with real. apply Rmult_lt_compat_l; auto with real. + apply pow_lt; auto with real. apply Rlt_trans with (r2 := 1); auto with real. + apply Rlt_minus; auto with real. apply Rlt_pow_R1; [ | apply lt_minus_O_lt ]; assumption. - apply Nat.sub_add, Nat.lt_le_incl; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac