proposition: Lemma IVT_interv_prelim1 : forall (x y x0:R) (D : R -> bool), x < y -> Un_cv (dicho_up x y D) x0 -> x <= x0 <= y.
proof: Proof. intros x y x0 D x_lt_y bnd. assert (Main : forall n, x <= dicho_up x y D n <= y). { intro n. unfold dicho_up. apply (proj1 (IVT_interv_prelim0 x y D n x_lt_y)). } split. - apply Rle_cv_lim with (Vn:=dicho_up x y D) (Un:=fun n => x). + intro n ; exact (proj1 (Main n)). + unfold Un_cv ; intros ; exists 0%nat ; intros ; unfold Rdist ; replace (x -x) with 0 by field ; rewrite Rabs_R0 ; assumption. + assumption. - apply Rle_cv_lim with (Un:=dicho_up x y D) (Vn:=fun n => y). + intro n ; exact (proj2 (Main n)). + assumption. + unfold Un_cv ; intros ; exists 0%nat ; intros ; unfold Rdist ; replace (y -y) with 0 by field ; rewrite Rabs_R0 ; assumption. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra