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