proposition: Lemma dicho_steps_interval_compat : forall x y P N, x <= y -> interval x y (dicho_up x y P N) /\ interval x y (dicho_lb x y P N).
proof: Proof. intros x y P N x_le_y ; induction N. simpl ; split ; [apply interval_r | apply interval_l] ; assumption. simpl ; split ; fold (middle (Dichotomy_lb x y P N) (Dichotomy_ub x y P N)) ; destruct (P (middle (Dichotomy_lb x y P N) (Dichotomy_ub x y P N))) ; try apply interval_middle_compat ; apply IHN. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity