proposition: Lemma interval_minus_compat_0 : forall lb ub x, interval lb ub x -> interval (lb - x) (ub - x) 0.
proof: Proof. intros lb ub x ; replace 0 with (x - x) by ring ; apply interval_minus_compat. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics