proposition: Lemma open_interval_dist_pos: forall lb ub x, open_interval lb ub x -> 0 < interval_dist lb ub x.
proof: Proof. intros lb ub x [x_lb x_ub] ; apply Rmin_pos_lt ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics