proposition: Lemma dense_Rball : forall c r x, Rball c r x -> dense (Rball c r) x.
proof: Proof. intros c r x x_in eps eps_pos ; assert (r_pos : 0 < r) by (eapply Rball_radius_pos ; eassumption) ; assert (Hlbub : c - r < c + r) by lra ; assert (x_in' : interval (c - r) (c + r) x). apply open_interval_interval, included_Rball_open_interval ; assumption. destruct (dense_open_interval (c - r) (c + r) x Hlbub x_in' eps eps_pos) as [y [[y_in y_neq] Hy]] ; exists y ; repeat split ; [apply included_open_interval_Rball2 | |] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra