proposition: Lemma in_holed_interval_dec (a b h : R) (u : nat -> R) (n : nat) : {in_holed_interval a b h u n} + {~in_holed_interval a b h u n}.
proof: Proof. destruct (total_order_T a (u n)) as [[l|e]|hi]. - destruct (total_order_T b (u n)) as [[lb|eb]|hb]. + right. intro H. destruct H. destruct H0. apply Rlt_asym in H0. contradiction. + subst. right. intro H. destruct H. destruct H0. pose proof (Rlt_asym (u n) (u n) H0). contradiction. + destruct (Req_dec_T h (u n)). * subst. right. intro H. destruct H. destruct H0. exact (H1 eq_refl). * left. split. -- assumption. -- split. ++ assumption. ++ intro H. subst. exact (n0 eq_refl). - subst. right. intro H. destruct H. pose proof (Rlt_asym (u n) (u n) H). contradiction. - right. intro H. destruct H. apply Rlt_asym in H. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon