proposition: Lemma Rseq_cv_pos_infty_inv_compat : Rseq_cv_pos_infty Un -> Rseq_cv (/ Un) 0.
proof: Proof. intros H eps Heps. destruct (H (/eps)%R) as [N HN]. exists N; intros n Hn. assert (Hpos : Un n > 0). eapply Rlt_trans; [|apply HN; assumption]. apply Rinv_0_lt_compat; assumption. unfold R_dist; unfold Rseq_inv. replace (/Un n - 0)%R with (/ Un n)%R; [|field; auto with real]. rewrite <- Rinv_inv. rewrite Rabs_inv. apply Rinv_lt_contravar. apply Rmult_gt_0_compat. apply Rinv_0_lt_compat; assumption. rewrite Rabs_right; [|left]; assumption. rewrite Rabs_right; [apply HN|left]; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra