Correctness of binary comparisons

The format-parameterized executable comparison agrees with exact dyadic, real, and extended-real order. The selection theorems also specify IEEE minimum and maximum, including infinities and signed-zero tie breaking.

All results are uniform in the binary format.

Classification helpers

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN2_none_of_not_isNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.chooseNaN2 y = none

NaN selection returns none when both inputs are known not to be NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_none_iff {fmt : FloatFormat} (x y : Model fmt) : x.compare y = none ↔ x.isNaN = true ∨ y.isNaN = true

Exactly pairs containing a NaN produce the unordered comparison relation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_eq_minimum_of_not_isNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.minNum y = x.minimum y

Without NaNs, minNum is exactly the ordinary IEEE minimum operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_eq_maximum_of_not_isNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.maxNum y = x.maximum y

Without NaNs, maxNum is exactly the ordinary IEEE maximum operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_of_isSNaN_left {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = true) : x.minNum y = x.quietNaN

A signaling left operand has first priority in minNum and is returned after quieting.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_of_isSNaN_right {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = false) (hy : y.isSNaN = true) : x.minNum y = y.quietNaN

When the left operand is not signaling, a signaling right operand has priority in minNum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_of_isNaN_left {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = true) (hyNaN : y.isNaN = false) : x.minNum y = y

After signaling NaNs are excluded, minNum skips one quiet NaN on the left.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_of_isNaN_right {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = true) : x.minNum y = x

After signaling NaNs are excluded, minNum skips one quiet NaN on the right.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_of_isNaN_both {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = true) (hyNaN : y.isNaN = true) : x.minNum y = x.quietNaN

When both operands are quiet NaNs, minNum quiets and returns the left operand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_of_isSNaN_left {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = true) : x.maxNum y = x.quietNaN

A signaling left operand has first priority in maxNum and is returned after quieting.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_of_isSNaN_right {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = false) (hy : y.isSNaN = true) : x.maxNum y = y.quietNaN

When the left operand is not signaling, a signaling right operand has priority in maxNum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_of_isNaN_left {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = true) (hyNaN : y.isNaN = false) : x.maxNum y = y

After signaling NaNs are excluded, maxNum skips one quiet NaN on the left.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_of_isNaN_right {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = true) : x.maxNum y = x

After signaling NaNs are excluded, maxNum skips one quiet NaN on the right.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_of_isNaN_both {fmt : FloatFormat} (x y : Model fmt) (hxSNaN : x.isSNaN = false) (hySNaN : y.isSNaN = false) (hxNaN : x.isNaN = true) (hyNaN : y.isNaN = true) : x.maxNum y = x.quietNaN

When both operands are quiet NaNs, maxNum quiets and returns the left operand.

IEEE 754-2019 minimumNumber and maximumNumber

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_eq_minimum_of_not_isNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.minimumNumber y = x.minimum y

Without NaNs, minimumNumber is exactly the IEEE minimum operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_eq_maximum_of_not_isNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.maximumNumber y = x.maximum y

Without NaNs, maximumNumber is exactly the IEEE maximum operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_of_isNaN_left {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = true) (hy : y.isNaN = false) : x.minimumNumber y = y

minimumNumber returns the right operand whenever only the left operand is a NaN, even a signaling one. This is the point where IEEE 754-2019 departs from minNum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_of_isNaN_right {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = true) : x.minimumNumber y = x

minimumNumber returns the left operand whenever only the right operand is a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_of_isNaN_both {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = true) (hy : y.isNaN = true) : x.minimumNumber y = x.bothNaNNumber y

When both operands are NaNs, minimumNumber delivers the quiet NaN chosen by bothNaNNumber.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_of_isNaN_left {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = true) (hy : y.isNaN = false) : x.maximumNumber y = y

maximumNumber returns the right operand whenever only the left operand is a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_of_isNaN_right {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = true) : x.maximumNumber y = x

maximumNumber returns the left operand whenever only the right operand is a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_of_isNaN_both {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = true) (hy : y.isNaN = true) : x.maximumNumber y = x.bothNaNNumber y

When both operands are NaNs, maximumNumber delivers the quiet NaN chosen by bothNaNNumber.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bothNaNNumber_eq_or {fmt : FloatFormat} (x y : Model fmt) : x.bothNaNNumber y = x.quietNaN ∨ x.bothNaNNumber y = y.quietNaN

The NaN chosen for two NaN operands is always one of them, quieted.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_eq_minNum_of_not_isSNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = false) (hy : y.isSNaN = false) : x.minimumNumber y = x.minNum y

When neither operand is a signaling NaN, minimumNumber agrees with minNum, including when one or both operands are quiet NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_eq_maxNum_of_not_isSNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isSNaN = false) (hy : y.isSNaN = false) : x.maximumNumber y = x.maxNum y

The maximumNumber counterpart of minimumNumber_eq_minNum_of_not_isSNaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq_zero_of_isZero {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.toReal = 0

The real interpretation erases the sign of an executable zero.

Non-NaN minimum and maximum

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_minimum_eq_false_of_isNaN_eq_false {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minimum y).isNaN = false

IEEE minimum is non-NaN when both operands are non-NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_maximum_eq_false_of_isNaN_eq_false {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maximum y).isNaN = false

IEEE maximum is non-NaN when both operands are non-NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_minimumNumber_eq_false_of_not_both {fmt : FloatFormat} (x y : Model fmt) (h : x.isNaN = false ∨ y.isNaN = false) : (x.minimumNumber y).isNaN = false

minimumNumber never returns a NaN unless both operands are NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_maximumNumber_eq_false_of_not_both {fmt : FloatFormat} (x y : Model fmt) (h : x.isNaN = false ∨ y.isNaN = false) : (x.maximumNumber y).isNaN = false

maximumNumber never returns a NaN unless both operands are NaNs.

Finite comparison

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_compareNonNaN {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.compare y = some (x.compareNonNaN y hx hy)

Once both operands are known not to be NaNs, the public comparison is exactly the total non-NaN comparison.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compareNonNaN_eq_of_compare_eq_some {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) {order : Ordering} (hcompare : x.compare y = some order) : x.compareNonNaN y hx hy = order

Any successful public comparison determines the result of the total non-NaN comparison.

This is the proof bridge used by the min/max semantics below: runtime code does not need an unreachable unordered branch once NaNs have already been excluded.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_cmpDyadic_of_toDyadic? {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some (cmpDyadic dx dy)

When both operands decode to dyadics, executable comparison returns their exact dyadic ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_lt_iff_toReal_lt {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.lt ↔ x.toReal < y.toReal

Finite executable comparison returns .lt exactly when the decoded reals are ordered.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_eq_iff_toReal_eq {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.eq ↔ x.toReal = y.toReal

Finite executable comparison returns .eq exactly when the decoded reals are equal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_gt_iff_toReal_gt {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.gt ↔ y.toReal < x.toReal

Finite executable comparison returns .gt exactly when the decoded reals are reversed.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_lt_iff_toReal_lt_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.lt ↔ x.toReal < y.toReal

On finite inputs, executable comparison agrees with strict real order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_eq_iff_toReal_eq_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.eq ↔ x.toReal = y.toReal

On finite inputs, executable comparison agrees with real equality.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_gt_iff_toReal_gt_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.compare y = some Ordering.gt ↔ y.toReal < x.toReal

On finite inputs, executable comparison agrees with reversed strict real order.

Signed-zero tie breaking

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_zero_false_true (fmt : FloatFormat) : (zero fmt false).compare (zero fmt true) = some Ordering.eq

Positive and policy-selected negative zero compare equal numerically.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimum_zero_false_true (fmt : FloatFormat) : (zero fmt false).minimum (zero fmt true) = zero fmt true

minimum selects policy-negative zero from a positive-zero/negative-zero tie.

In a format without signed zero, both inputs and the result are the single positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximum_zero_false_true (fmt : FloatFormat) : (zero fmt false).maximum (zero fmt true) = zero fmt false

maximum selects positive zero from a positive-zero/negative-zero tie.

In a format without signed zero, both inputs already denote the single positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimum_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).minimum (negZero fmt) = negZero fmt

For every encoding with signed zero, minimum (+0, -0) returns the negative zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximum_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).maximum (negZero fmt) = posZero fmt

For every encoding with signed zero, maximum (+0, -0) returns the positive zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNum_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).minNum (negZero fmt) = negZero fmt

For every encoding with signed zero, minNum (+0, -0) returns the negative zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maxNum_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).maxNum (negZero fmt) = posZero fmt

For every encoding with signed zero, maxNum (+0, -0) returns the positive zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).minimumNumber (negZero fmt) = negZero fmt

For every encoding with signed zero, minimumNumber (+0, -0) returns the negative zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber_posZero_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (posZero fmt).maximumNumber (negZero fmt) = posZero fmt

For every encoding with signed zero, maximumNumber (+0, -0) returns the positive zero encoding.

Finite minimum and maximum

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_minimum_eq_min {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.minimum y).toReal = min x.toReal y.toReal

On finite inputs, IEEE minimum agrees with real min.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_maximum_eq_max {fmt : FloatFormat} (x y : Model fmt) {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.maximum y).toReal = max x.toReal y.toReal

On finite inputs, IEEE maximum agrees with real max.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_minimum_eq_min_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).toReal = min x.toReal y.toReal

On finite inputs, IEEE minimum agrees with real min.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_maximum_eq_max_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).toReal = max x.toReal y.toReal

On finite inputs, IEEE maximum agrees with real max.

Extended-real comparison

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_toEReal?_of_isNaN_eq_false {fmt : FloatFormat} (x : Model fmt) (hx : x.isNaN = false) : ∃ (value : EReal), x.toEReal? = some value

Every non-NaN executable value has a partial extended-real interpretation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal?_cases {fmt : FloatFormat} (x : Model fmt) {value : EReal} (hx : x.toEReal? = some value) : (x.isInf = true ∧ value = if x.signBit = true then ⊥ else ⊤) ∨ x.isFinite = true ∧ value = ↑x.toReal

Every successful extended-real interpretation is either a signed infinity or a finite real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_of_toEReal? {fmt : FloatFormat} {x y : Model fmt} {a b : EReal} (hx : x.toEReal? = some a) (hy : y.toEReal? = some b) : x.compare y = some (Ord.compare a b)

A non-NaN comparison returns the ordering of its exact extended-real values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_lt_iff_toEReal_lt {fmt : FloatFormat} {x y : Model fmt} {ex ey : EReal} (hx : x.toEReal? = some ex) (hy : y.toEReal? = some ey) : x.compare y = some Ordering.lt ↔ ex < ey

Non-NaN executable comparison agrees with strict extended-real order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_eq_iff_toEReal_eq {fmt : FloatFormat} {x y : Model fmt} {ex ey : EReal} (hx : x.toEReal? = some ex) (hy : y.toEReal? = some ey) : x.compare y = some Ordering.eq ↔ ex = ey

Non-NaN executable comparison agrees with extended-real equality.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_self_of_isNaN_eq_false {fmt : FloatFormat} (x : Model fmt) (h : x.isNaN = false) : x.compare x = some Ordering.eq

Every non-NaN value compares equal to itself.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compare_eq_some_gt_iff_toEReal_gt {fmt : FloatFormat} {x y : Model fmt} {ex ey : EReal} (hx : x.toEReal? = some ex) (hy : y.toEReal? = some ey) : x.compare y = some Ordering.gt ↔ ey < ex

Non-NaN executable comparison agrees with reversed strict extended-real order.

Extended-real minimum and maximum

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_eq_zero_of_isZero {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.toEReal = 0

The total extended-real interpretation erases the sign of an executable zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_minimum_eq_min {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minimum y).toEReal = min x.toEReal y.toEReal

IEEE minimum agrees with min on every pair of non-NaN extended-real values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_maximum_eq_max {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maximum y).toEReal = max x.toEReal y.toEReal

IEEE maximum agrees with max on every pair of non-NaN extended-real values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_minNum_eq_min {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minNum y).toEReal = min x.toEReal y.toEReal

On non-NaN values, minNum has the exact extended-real semantics of mathematical minimum. Signed-zero tie breaking remains visible in the encoded result even though toEReal identifies the two zeros.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_maxNum_eq_max {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maxNum y).toEReal = max x.toEReal y.toEReal

On non-NaN values, maxNum has the exact extended-real semantics of mathematical maximum. Signed-zero tie breaking remains visible in the encoded result even though toEReal identifies the two zeros.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_minimumNumber_eq_min {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minimumNumber y).toEReal = min x.toEReal y.toEReal

On non-NaN values, minimumNumber has the extended-real semantics of mathematical minimum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_maximumNumber_eq_max {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maximumNumber y).toEReal = max x.toEReal y.toEReal

On non-NaN values, maximumNumber has the extended-real semantics of mathematical maximum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_minimumNumber_comm {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.minimumNumber y).toEReal = (y.minimumNumber x).toEReal

minimumNumber is commutative up to extended-real value on non-NaN operands. This interpretation identifies the two signed zeros.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_maximumNumber_comm {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : (x.maximumNumber y).toEReal = (y.maximumNumber x).toEReal

The maximumNumber counterpart of toEReal_minimumNumber_comm.