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