proposition: Lemma Rball_radius_pos : forall c r x, Rball c r x -> 0 < r.
proof: Proof. unfold Rball ; intros c r x Hx ; eapply Rle_lt_trans ; [apply Rabs_pos | eassumption]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics