proposition: Lemma is_upper_bound_epsilon : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop), sig_forall_dec_T -> sig_not_dec_T -> (exists x:CRcarrier R, is_upper_bound E x) -> { n:nat | is_upper_bound E (CR_of_Q R (Z.of_nat n # 1)) }.
proof: Proof. intros R E lpo sig_not_dec Ebound. apply constructive_indefinite_ground_description_nat. - intro n. apply is_upper_bound_dec. + exact lpo. + exact sig_not_dec. - destruct Ebound as [x H]. destruct (CRup_nat x) as [n nmaj]. exists n. intros y ey. specialize (H y ey). apply (CRle_trans _ x _ H). apply CRlt_asym, nmaj. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon