proposition: Lemma cv_infty_cv_0 : forall Un:nat -> R, cv_infty Un -> Un_cv (fun n:nat => / Un n) 0.
proof: Proof. unfold cv_infty, Un_cv; unfold Rdist; intros Un H0 eps H1. elim (H0 (/ eps)); intros N0 H2. exists N0; intros n H3. unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_inv. destruct (Req_dec (Un n) 0) as [->|H]. { now rewrite Rabs_R0, Rinv_0. } apply Rmult_lt_reg_l with (Rabs (Un n)). - apply Rabs_pos_lt; apply H. - rewrite Rinv_r. + apply Rmult_lt_reg_l with (/ eps). * apply Rinv_0_lt_compat; assumption. * rewrite Rmult_1_r; rewrite (Rmult_comm (/ eps)); rewrite Rmult_assoc; rewrite Rinv_r. -- rewrite Rmult_1_r; apply Rlt_le_trans with (Un n). ++ apply H2; assumption. ++ apply RRle_abs. -- red; intro; rewrite H4 in H1; elim (Rlt_irrefl _ H1). + apply Rabs_no_R0; apply H. Qed.
imports: Rbase Rfunctions Rseries Lia