proposition: Lemma pow_lt_1_zero : forall x:R, Rabs x < 1 -> forall y:R, 0 < y -> exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).
proof: Proof. intros; elim (Req_dec x 0); intro. - exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero. + rewrite Rabs_R0; assumption. + inversion GE; auto. - assert (Rabs (/ x) > 1). { rewrite <- (Rinv_inv 1). rewrite Rabs_inv. unfold Rgt; apply Rinv_lt_contravar. - apply Rmult_lt_0_compat. + apply Rabs_pos_lt. assumption. + rewrite Rinv_1; apply Rlt_0_1. - rewrite Rinv_1; assumption. } elim (Pow_x_infinity (/ x) H2 (/ y + 1)); intros N. exists N; intros; rewrite <- (Rinv_inv y). rewrite <- (Rinv_inv (Rabs (x ^ n))). apply Rinv_lt_contravar. + apply Rmult_lt_0_compat. * apply Rinv_0_lt_compat. assumption. * apply Rinv_0_lt_compat. apply Rabs_pos_lt. apply pow_nonzero. assumption. + rewrite <- Rabs_inv, <- pow_inv. apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))). * pattern (/ y) at 1. rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1). apply Rplus_lt_compat_l. apply Rlt_0_1. * apply Rge_le. apply H3. assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac