def IntegerLongDivision.longDivStep (b : ℕ) (bit : Bool) (qr : ℕ × ℕ) : ℕ × ℕ

One step of binary long division by b: given the current quotient/remainder pair qr and the next bit bit of the dividend, shift the partial quotient/remainder left by one (i.e., multiply by 2), add bit to the remainder, and conditionally subtract b to keep the remainder smaller than b.

def IntegerLongDivision.longDivLoop (a b m : ℕ) : ℕ → ℕ × ℕ

Recursive driver of binary long division: starting from the most significant bit m of a, folds longDivStep over k+1 iterations consuming successive bits from m down to m - k - 1. The result is the quotient/remainder pair after processing those bits.

def IntegerLongDivision.longDiv (a b m : ℕ) : ℕ × ℕ

Schoolbook binary long division of a by b, treating a as an (m+1)-bit number: returns the quotient/remainder pair after processing all bits from position m down to 0.

theorem IntegerLongDivision.testBit_toNat_eq_mod_two (n k : ℕ) : (n.testBit k).toNat = n / 2 ^ k % 2

The k-th bit of n (as a Nat) equals n / 2 ^ k mod 2.

theorem IntegerLongDivision.div_pow_two_step (a k : ℕ) : a / 2 ^ k = 2 * (a / 2 ^ (k + 1)) + (a.testBit k).toNat

Bit-shift identity for integer division: a / 2^k = 2 * (a / 2^(k+1)) + bit_k(a). This is the key relation that makes binary long division advance by exactly one bit per step.

theorem IntegerLongDivision.longDivStep_invariant (b : ℕ) (bit : Bool) (q r : ℕ) (hr : r < b) : have res := longDivStep b bit (q, r); res.1 * b + res.2 = 2 * (q * b + r) + bit.toNat ∧ res.2 < b

Single-step invariant for longDivStep: if the incoming remainder r is < b, then the output pair (q', r') satisfies q' * b + r' = 2 * (q * b + r) + bit and r' < b.

theorem IntegerLongDivision.longDivLoop_invariant (a b m : ℕ) (hb : 0 < b) (ham : a < 2 ^ (m + 1)) (k : ℕ) : k ≤ m → have res := longDivLoop a b m k; res.1 * b + res.2 = a / 2 ^ (m - k) ∧ res.2 < b

Loop invariant for longDivLoop: after processing k+1 bits, the result pair (q, r) satisfies q * b + r = a / 2^(m - k) and r < b. This expresses that the loop computes the correct partial quotient/remainder for the top k+1 bits of a.

theorem IntegerLongDivision.long_division_correct (a b m : ℕ) (hb : 0 < b) (ham : a < 2 ^ (m + 1)) : have res := longDiv a b m; a = res.1 * b + res.2 ∧ res.2 < b

Correctness of longDiv: for 0 < b and a < 2^(m+1), the result (q, r) = longDiv a b m satisfies a = q * b + r with r < b, i.e., it computes the integer quotient and remainder.

def IntegerLongDivision.longDivNat (a b : ℕ) : ℕ × ℕ

Natural-number long division specialized to the bit-length of a: uses Nat.log 2 a as the top bit index, yielding a quotient/remainder pair for a / b.