theorem e_lt_of_lt (a b : PackedFloat 5 2) : lt a b = true ↔ e_lt (a.toEFixed ⋯) (b.toEFixed ⋯) = true

theorem le_of_e_le (m : RoundingMode) (a b : EFixedPoint 35 16) : e_le a b = true → le (round 5 2 m a) (round 5 2 m b) = true

theorem e_le_of_le (a b : PackedFloat 5 2) : le a b = true → e_le (a.toEFixed ⋯) (b.toEFixed ⋯) = true

theorem toEFixed_isExactFloat (a : PackedFloat 5 2) : isExactFloat 5 2 (a.toEFixed ⋯) = true

Every floating point number converted to fixed point form, is an exact floating point number.

theorem isExactFloat_round_toEFixed (a : EFixedPoint 34 16) (m : RoundingMode) (ha : isExactFloat 5 2 a = true) : a.equal_denotation ((round 5 2 m a).toEFixed ⋯) = true

If a fixed point number is an exact floating point number, then converting to floating point and back should not change the denotation.

theorem round_leftinv_toEFixed (x : PackedFloat 5 2) (mode : RoundingMode) (hx : ¬x.isNaN = true) : round 5 2 mode (x.toEFixed ⋯) = x

Fixed -> Float rounding is left inverse to Float -> Fixed conversion

theorem f_add_comm (m : RoundingMode) (a b : FixedPoint 34 16) : f_add m a b = f_add m b a

theorem e_add_comm (m : RoundingMode) (a b : EFixedPoint 34 16) : e_add m a b = e_add m b a

theorem add_comm (m : RoundingMode) (a b : PackedFloat 5 2) : add ⋯ a b m = add ⋯ b a m

theorem add_neg_self_isZero_or_isNaN (a : PackedFloat 5 2) (m : RoundingMode) : (add ⋯ a (neg a) m).isZero = true ∨ (add ⋯ a (neg a) m).isNaN = true

theorem add_zero_is_id (a : PackedFloat 5 2) (m : RoundingMode) (ha : ¬a.isNaN = true ∧ ¬a.isZero = true) : add ⋯ a (PackedFloat.getZero 5 2) m = a

theorem e_add_monotone (m : RoundingMode) (a b c : EFixedPoint 34 16) (hc : c.state = State.Number) : e_le a b = true → e_le (e_add m a c) (e_add m b c) = true

theorem add_monotone (a b c : PackedFloat 5 2) (m : RoundingMode) (hc : c.isNormOrSubnorm = true) : le a b = true → le (add ⋯ a c m) (add ⋯ b c m) = true

theorem sterbenz (a b : PackedFloat 5 2) (h : le a (doubleRNE b) = true ∧ le b (doubleRNE a) = true) : isExactFloat 5 2 (e_add RoundingMode.RTZ (a.toEFixed ⋯) ((neg b).toEFixed ⋯)) = true

A floating-point subtraction is computed exactly iff the operands are within a factor of two of each other.

• https://en.wikipedia.org/wiki/Sterbenz_lemma

theorem mul_comm (a b : PackedFloat 5 2) (m : RoundingMode) : mul a b m = mul b a m

theorem mul_one_is_id (a : PackedFloat 5 2) (m : RoundingMode) (ha : ¬a.isNaN = true) : mul a oneE5M2 m = a

theorem add_eq_mul_two (a : PackedFloat 5 2) (m : RoundingMode) : add ⋯ a a m = mul twoE5M2 a m

theorem doubleRNE_eq_mul_two (a : PackedFloat 5 2) : doubleRNE a = mul twoE5M2 a RoundingMode.RNE

theorem f_mul_comm (a b : FixedPoint 34 16) : f_mul a b = f_mul b a

theorem e_mul_comm (a b : EFixedPoint 34 16) : e_mul a b = e_mul b a

theorem mulfixed_comm (a b : PackedFloat 5 2) (m : RoundingMode) : mulfixed ⋯ a b m = mulfixed ⋯ b a m

theorem div_one_is_id (a : PackedFloat 5 2) (h : ¬a.isNaN = true) : div a oneE5M2 RoundingMode.RTZ = a

theorem div_self_is_one (a : PackedFloat 5 2) (h : ¬a.isNaN = true ∧ ¬a.isInfinite = true ∧ ¬a.isZero = true) : div a a RoundingMode.RTZ = oneE5M2

theorem sterbenzFP16 (a b : PackedFloat 5 10) (h : le a (doubleRNE b) = true ∧ le b (doubleRNE a) = true) : isExactFloat 5 10 (e_add RoundingMode.RTZ (a.toEFixed ⋯) ((neg b).toEFixed ⋯)) = true