proposition: Lemma Rball_0_simpl: forall r x, Rball 0 r x <-> Rabs x < r.
proof: Proof. intros ; unfold Rball ; rewrite Rminus_0_r ; split ; trivial. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics