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