proposition: Lemma Rseq_cv_0_pos_maj_compat : forall Un Vn, (forall n, 0 <= Un n) -> (forall n, Un n <= Vn n) -> Rseq_cv Vn 0 -> Rseq_cv Un 0.
proof: Proof. intros Un Vn Unpos Unmaj Vncv e epos. destruct (Vncv e epos) as [N H]. exists N; intros n nN. unfold R_dist; rewrite Rminus_0_r; rewrite Rabs_pos_eq; [|apply Unpos]. eapply Rle_lt_trans. apply Unmaj. pose proof H n nN as J. unfold R_dist in J; rewrite Rminus_0_r in J; rewrite Rabs_pos_eq in J. apply J. eapply Rle_trans; [apply Unpos | apply Unmaj]. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith