Order bounds for roundQuotEven

IEEE32Exec.roundRatToIEEE32 rounds an exact rational num/den to binary32 using round-to-nearest, ties-to-even.

At the integer level it relies on:

roundQuotEven num den : Nat

which rounds the rational quotient to the nearest integer (ties-to-even), assuming den > 0.

For later "nearest vs directed" arguments, we only need the simple fact that roundQuotEven num den is always either the floor quotient q = num / den or the next integer q+1. This is the exact analogue of roundShiftRightEven_eq_q_or_q_add1 for the power-of-two division case.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundQuotEven_eq_div_or_div_add1 (num den : ℕ) : roundQuotEven num den = num / den ∨ roundQuotEven num den = num / den + 1

roundQuotEven num den is either the floor quotient num/den or that value plus one.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.div_le_roundQuotEven (num den : ℕ) : num / den ≤ roundQuotEven num den

Lower bound: the floor quotient is at most roundQuotEven num den.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundQuotEven_le_div_add1 (num den : ℕ) : roundQuotEven num den ≤ num / den + 1

Upper bound: roundQuotEven num den is at most the floor quotient plus one.