proposition: Lemma Rball_rewrite2: forall lb ub x, Rball (middle lb ub) (interval_size lb ub) x <-> open_interval lb ub x.
proof: Proof. intros ; split ; [apply included_Rball_open_interval2 | apply included_open_interval_Rball]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics