proposition: Lemma interval_open_interval_dec: forall lb ub x, interval lb ub x -> { x = lb } + { open_interval lb ub x } + { x = ub }.
proof: Proof. intros lb ub x [H1 H2]. destruct (Req_dec x lb). left ; left ; assumption. destruct (Req_dec x ub). right ; assumption. left ; right ; split. apply Rneq_le_lt ; [symmetry |] ; assumption. apply Rneq_le_lt ; assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics