proposition: Lemma dicho_diff_cv : forall x y P, x <= y -> Rseq_cv (dicho_up x y P - dicho_lb x y P) 0.
proof: Proof. intros x y P xley ; eapply Rseq_cv_eq_compat. intro n ; apply dicho_lb_dicho_up ; assumption. eapply Rseq_cv_pos_infty_div_compat, Rseq_constant_cv. apply Rseq_pow_gt_1_cv ; lra. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity