proposition: Lemma CR_sig_lub : forall {R : ConstructiveReals} (E:CRcarrier R -> Prop), (forall x y : CRcarrier R, CReq R x y -> (E x <-> E y)) -> sig_forall_dec_T -> sig_not_dec_T -> (exists x : CRcarrier R, E x) -> (exists x : CRcarrier R, CRis_upper_bound E x) -> { u : CRcarrier R | CRis_upper_bound E u /\ forall y:CRcarrier R, CRis_upper_bound E y -> CRlt R y u -> False }.
proof: Proof. intros. exact (sig_lub E X X0 H0 H1). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon