def est_lo
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as W64import Base
320# Knuth's estimate for x = xh * 2^64 + xl < b * 2^32 and b >= 2^32, t =
321# bits(hi(b)): with Y = x >> t (below 2^64) and B = b >> t in [2^31, 2^32),
322# min(floor(Y / B), 2^32 - 1) is at least floor(x / b) (as B 2^t <= b) and at
323# most 2 over it (Theorem B), so q_start takes a step or two
324def est_lo(+q1: Nat, +t2: Nat, +d: Nat) -> U32:
325 U32.from_nat(Nat.add(Nat.mul(q1, 65536n), Nat.div(t2, d)))