proposition: Lemma open_interval_interval : forall lb ub x, open_interval lb ub x -> interval lb ub x.
proof: Proof. intros ; split ; unfold open_interval in * ; intuition (auto with real). Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics