proposition: Lemma l_in_segment : lb <= l <= ub.
proof: Proof. destruct (l_in_Dn 0) as [Hl Hr]; split. eapply Rle_trans; [|apply Hl]. simpl; unfold succ. destruct (total_order_T (middle lb ub) (Rn 0)) as [[_|_]|_]; simpl; try apply Rle_refl. left; apply Rlt_middle_l; apply not_empty. eapply Rle_trans; [apply Hr|]. simpl; unfold succ. destruct (total_order_T (middle lb ub) (Rn 0)) as [[_|_]|_]; simpl; try apply Rle_refl. left; apply Rlt_middle_r; apply not_empty. left; eapply Rlt_trans; apply Rlt_middle_r. apply Rlt_middle_l; apply not_empty. apply not_empty. Qed.
imports: Reals Lra