fact: Definition is_lub (E:R -> Prop) (m:R) := is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions