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