proposition: Lemma open_interval_inhabited : forall lb ub x, open_interval lb ub x -> lb < ub.
proof: Proof. intros ; etransitivity ; eapply_assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics