proposition: Lemma in_Rball_dec: forall c r x, { Rball c r x } + { ~ Rball c r x }.
proof: Proof. intros c r x ; destruct (in_open_interval_dec (c - r) (c + r) x) as [Ht | Hf]. left ; rewrite Rball_rewrite ; assumption. right ; intro ; eapply Hf ; rewrite <- Rball_rewrite ; eassumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics