proposition: Lemma Rseq_cv_neg_infty_inv_compat : Rseq_cv_neg_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 Ropp_lt_gt_0_contravar; 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. apply Rabs_pos_lt; apply Rlt_not_eq; assumption. rewrite Rabs_left; [|assumption]. pattern (/ eps)%R; rewrite <- Ropp_involutive. apply Ropp_gt_lt_contravar. apply HN; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra