proposition: Lemma interval_size_pos : forall lb ub, lb < ub -> 0 < interval_size lb ub.
proof: Proof. unfold interval_size. intros ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics