Low-level rational rounding primitives

Format-independent executable quotient operations support nearest-even and directed rational rounding. The quotient layer stays below Model.Arithmetic, allowing native arithmetic kernels to reuse their proofs without creating an import cycle through the public dispatcher.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.quotCeil (numerator denominator : Nat) : Nat

Ceiling of a natural quotient, totalized to zero at a zero denominator.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected (roundUp : Bool) (numerator denominator : Nat) : Nat

Round a nonnegative quotient to an integer, selecting floor or ceiling.