proposition: Lemma in_open_interval_dec: forall lb ub x, { open_interval lb ub x } + { ~ open_interval lb ub x }.
proof: Proof. intros lb ub x. destruct (Rlt_le_dec lb x). destruct (Rlt_le_dec x ub). left ; split ; assumption. right ; intros [_ Hf] ; lra. right ; intros [Hf _] ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics