proposition: Lemma interval_size_Boule_middle : forall lb ub c pr, open_interval lb ub c -> Boule (middle lb ub) (mkposreal _ (interval_size_pos lb ub pr)) c.
proof: Proof. intros lb ub c pr [c_lb c_ub] ; apply Rabs_def1 ; unfold middle, pos, interval_size. apply Rlt_le_trans with (ub - (lb + ub) / 2). apply Rplus_lt_compat_r ; assumption. right ; field. apply Rle_lt_trans with (lb - (lb + ub) / 2). right ; field. apply Rplus_lt_compat_r ; assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def Rseries_def Lra RiemannInt SeqProp PeanoNat RIneq MyRIneq Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval RIVT Rsequence_def