proposition: Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat), x < y -> x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.
proof: Proof. assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub) by (intros;lra). intros x y P N x_lt_y. induction N. { simpl ; intuition. } simpl. case (P ((Dichotomy_lb x y P N + Dichotomy_ub x y P N) / 2)). { split. { apply Sublemma ; intuition. } intuition. } split. { intuition. } apply Sublemma ; intuition. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra