proposition: Lemma interval_minus_compat : forall lb ub x y, interval lb ub x -> interval (lb - y) (ub - y) (x - y).
proof: Proof. intros lb ub x y [Hlb Hub] ; split ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics