proposition: Lemma Rball_rewrite: forall c r x, Rball c r x <-> open_interval (c - r) (c + r) x.
proof: Proof. intros ; split ; [apply included_Rball_open_interval | apply included_open_interval_Rball2]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics