proposition: Lemma Rball_c_0_empty: forall c r x, r <= 0 -> ~ Rball c r x.
proof: Proof. intros c r x Hr Hf ; eapply (Rlt_irrefl 0). eapply Rle_lt_trans ; [eapply Rabs_pos |]. eapply Rlt_le_trans ; [eapply Hf | eassumption]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics