proposition: Lemma Power_monotonic : forall (x:R) (m n:nat), Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).
proof: Proof. intros x m n H; induction n as [| n Hrecn]; intros; inversion H0. - unfold Rle; right; reflexivity. - unfold Rle; right; reflexivity. - apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))). + apply Hrecn; assumption. + simpl; rewrite Rabs_mult. pattern (Rabs (x ^ n)) at 1. rewrite <- Rmult_1_r. rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))). apply Rmult_le_compat_l. * apply Rabs_pos. * unfold Rgt in H. apply Rlt_le; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac