proposition: Lemma Rseq_cv_0_inv_compat : Rseq_cv Un 0 -> Rseq_neq_0 Un -> Rseq_cv_pos_infty (|/ Un|).
proof: Proof. intros Hcv He M. pose (Mp := Rmax 1 M). assert (Hp : Mp > 0). eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. destruct (Hcv (/ Mp)%R) as [N HN]. apply Rinv_0_lt_compat; assumption. exists N; intros n Hn. apply Rle_lt_trans with Mp; [apply RmaxLess2|]. pattern Mp; rewrite <- Rinv_inv. assert (Hd : Un n <> 0). apply He. unfold Rseq_abs, Rseq_inv. rewrite Rabs_inv. apply Rinv_lt_contravar. apply Rmult_lt_0_compat; [|auto with real]. apply Rabs_pos_lt; assumption. replace (Un n) with (Un n - 0)%R by field. apply HN; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra