proposition: Lemma RinvN_cv : Un_cv RinvN 0.
proof: Proof. unfold Un_cv; intros; assert (H0 := archimed (/ eps)); elim H0; clear H0; intros; assert (H2 : (0 <= up (/ eps))%Z). { apply le_IZR; left; apply Rlt_trans with (/ eps); [ apply Rinv_0_lt_compat; assumption | assumption ]. } elim (IZN _ H2); intros; exists x; intros; unfold Rdist; simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; assert (H5 : 0 < INR n + 1). { apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ]. } rewrite Rabs_right; [ idtac | left; change (0 < / (INR n + 1)); apply Rinv_0_lt_compat; assumption ]; apply Rle_lt_trans with (/ (INR x + 1)). { apply Rinv_le_contravar. { apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ]. } apply Rplus_le_compat_r; apply le_INR; apply H4. } rewrite <- (Rinv_inv eps). apply Rinv_lt_contravar. { apply Rmult_lt_0_compat. { apply Rinv_0_lt_compat; assumption. } apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ]. } apply Rlt_trans with (INR x); [ rewrite INR_IZR_INZ; rewrite <- H3; apply H0 | pattern (INR x) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1 ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra