proposition: Lemma Rball_dist_pos: forall c r x, Rball c r x -> 0 < Rball_dist c r x.
proof: Proof. intros ; eapply open_interval_dist_pos, included_Rball_open_interval ; eassumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics