Compiler.NaturalMagnitudeArithmetic

405def magnitudeDivModNonzero =
406  (lambda unrestricted dividend : Bytes .
407    (lambda unrestricted divisor : Bytes .
408      (app
409        (lambda unrestricted result : (sigma unrestricted quotient : BytesBuilder . Bytes) .
410          (pair
411            (sigma unrestricted quotient : Bytes . Bytes)
412            (magnitudeNormalize (bytes-builder-build (first result)))
413            (second result)))
414        (bytes-eliminate
415          (lambda unrestricted rest : Bytes . (sigma unrestricted quotient : BytesBuilder . Bytes))
416          (pair (sigma unrestricted quotient : BytesBuilder . Bytes) (bytes-builder-empty) b"")
417          (lambda unrestricted head : Byte .
418            (lambda unrestricted tail : Bytes .
419              (lambda unrestricted prefix : (sigma unrestricted quotient : BytesBuilder . Bytes) .
420                (magnitudeDivideStep divisor head prefix))))
421          dividend))))