proposition: Lemma cv_dicho : forall (x y l1 l2:R) (P:R -> bool), x <= y -> Un_cv (dicho_lb x y P) l1 -> Un_cv (dicho_up x y P) l2 -> l1 = l2.
proof: Proof. intros. assert (H2 := CV_minus _ _ _ _ H0 H1). cut (Un_cv (fun i:nat => dicho_lb x y P i - dicho_up x y P i) 0). { intro. assert (H4 := UL_sequence _ _ _ H2 H3). apply Rminus_diag_uniq; assumption. } unfold Un_cv; unfold Rdist. intros. assert (H4 := cv_infty_cv_0 pow_2_n pow_2_n_infty). destruct (total_order_T x y) as [[ Hlt | -> ]|Hgt]. 2:{ exists 0%nat; intros. replace (dicho_lb y y P n - dicho_up y y P n - 0) with (dicho_lb y y P n - dicho_up y y P n); [ idtac | ring ]. rewrite <- Rabs_Ropp. rewrite Ropp_minus_distr. rewrite dicho_lb_dicho_up. - unfold Rminus, Rdiv; rewrite Rplus_opp_r; rewrite Rmult_0_l; rewrite Rabs_R0; assumption. - assumption. } 2:{ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). } unfold Un_cv in H4; unfold Rdist in H4. assert (Hyp:0 < y - x) by lra. assert (0 < eps / (y - x)). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; assumption ]. } elim (H4 (eps / (y - x)) H5); intros N H6. exists N; intros. replace (dicho_lb x y P n - dicho_up x y P n - 0) with (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ]. rewrite <- Rabs_Ropp. rewrite Ropp_minus_distr. rewrite dicho_lb_dicho_up. 2:lra. unfold Rdiv; rewrite Rabs_mult. rewrite (Rabs_right (y - x)). 2:lra. apply Rmult_lt_reg_l with (/ (y - x)). { apply Rinv_0_lt_compat; assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. 2:lra. rewrite Rmult_1_l. replace (/ 2 ^ n) with (/ 2 ^ n - 0); [ unfold pow_2_n, Rdiv in H6; rewrite <- (Rmult_comm eps); apply H6; assumption | ring ]. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra