proposition: Lemma Rle_cv_lim : forall (Un Vn:nat -> R) (l1 l2:R), (forall n:nat, Un n <= Vn n) -> Un_cv Un l1 -> Un_cv Vn l2 -> l1 <= l2.
proof: Proof. intros; destruct (Rle_dec l1 l2) as [Hle|Hnle]. { assumption. } assert (H2 : l2 < l1). { auto with real. } assert (H3 : 0 < (l1 - l2) / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply Rlt_0_minus; assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H1 _ H3); elim (H0 _ H3); clear H0 H1; unfold Rdist; intros; set (N := max x x0); cut (Vn N < Un N). { intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (H N) H4)). } apply Rlt_trans with ((l1 + l2) / 2). { apply Rplus_lt_reg_l with (- l2); replace (- l2 + (l1 + l2) / 2) with ((l1 - l2) / 2). { rewrite Rplus_comm; apply Rle_lt_trans with (Rabs (Vn N - l2)). { apply RRle_abs. } apply H1; unfold ge; unfold N; apply Nat.le_max_r. } lra. } apply Ropp_lt_cancel; apply Rplus_lt_reg_l with l1; replace (l1 + - ((l1 + l2) / 2)) with ((l1 - l2) / 2). { apply Rle_lt_trans with (Rabs (Un N - l1)). { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. } apply H0; unfold ge; unfold N; apply Nat.le_max_l. } lra. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra