proposition: Lemma middle_r_in_Rball : forall c r, 0 < r -> Rball c r (middle c (c + r)).
proof: Proof. intros c r r_pos ; apply included_open_interval_Rball2 ; split. transitivity c. lra. apply middle_is_in_the_middle ; lra. apply middle_is_in_the_middle ; lra. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra