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