proposition: Lemma is_upper_bound_not_epsilon : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop), sig_forall_dec_T -> sig_not_dec_T -> (exists x : CRcarrier R, E x) -> { m:nat | ~is_upper_bound E (-CR_of_Q R (Z.of_nat m # 1)) }.
proof: Proof. intros R E lpo sig_not_dec H. apply constructive_indefinite_ground_description_nat. - intro n. destruct (is_upper_bound_dec E (-CR_of_Q R (Z.of_nat n # 1)) lpo sig_not_dec). + right. intro abs. contradiction. + left. exact n0. - destruct H as [x H]. destruct (CRup_nat (-x)) as [n H0]. exists n. intro abs. specialize (abs x H). apply abs. rewrite <- (CRopp_involutive x). apply CRopp_gt_lt_contravar. exact H0. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon