The real numbers are an Archimedean floor ring, and a conditionally complete linear order. #
0 is the default value for
Real.sSup of the empty set or sets which are not bounded above, it
suffices to show that all elements of
S are bounded by a nonnegative number to show that
is bounded by this number.
instance Real.instIsCompleteRealInstLinearOrderedFieldRealInstRingRealAbsToHasAbsInstNegRealInstSupRealAbs_isAbsoluteValueInstLinearOrderedRingReal :