proposition: Lemma Rle_pow : forall (x:R) (m n:nat), 1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n.
proof: Proof. intros. replace n with (n - m + m)%nat. - rewrite pow_add. rewrite Rmult_comm. pattern (x ^ m) at 1; rewrite <- Rmult_1_r. apply Rmult_le_compat_l. + apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ]. + apply pow_R1_Rle; assumption. - apply Nat.sub_add; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac