proposition: Lemma dicho_interval_compat : forall x y l P, x <= y -> Rseq_cv (dicho_up x y P) l -> interval x y l.
proof: Proof. intros x y l P x_le_y Hl ; eapply Rseq_interval_compat ; [| eassumption] ; intro ; apply dicho_steps_interval_compat ; assumption. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity