proposition: Lemma is_upper_bound_dec : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop) (x:CRcarrier R), sig_forall_dec_T -> sig_not_dec_T -> { is_upper_bound E x } + { ~is_upper_bound E x }.
proof: Proof. intros R E x lpo sig_not_dec. destruct (sig_not_dec (~exists y:CRcarrier R, E y /\ CRltProp R x y)). - left. intros y H. destruct (CRlt_lpo_dec x y lpo). 2: exact c. exfalso. apply n. intro abs. apply abs. clear abs. exists y. split. + exact H. + apply CRltForget. exact c. - right. intro abs. apply n. intros [y [H H0]]. specialize (abs y H). apply CRltEpsilon in H0. contradiction. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon