Size bounds when the leading quotient of a continued fraction is at least one

Proved

burau_cf_sub_bounds_ge_one

by lt9 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcontinued-fractionseuclidean-algorithm

Size bounds for a rational whose leading continued-fraction quotient is at least $1$ . For integers $a>0$ and $b$ with $b/a\ge 1$ (integer division), one has

0\le b-a < b .

This is the elementary bound that lets the negative-divisor Euclidean identities be phrased uniformly and is used, with the quotient and remainder formulas for a negated dividend, to obtain the first step of the negative-reciprocal rule of continued fractions.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem burau_cf_sub_bounds_ge_one (a b : ℤ) (ha : 0 < a) (h : 1 ≤ b / a) :
    0 ≤ b - a ∧ b - a < b := by sorry

Source

Euclidean continued fractions; cf. A. Ya. Khinchin, *Continued Fractions* (1964), Ch. II.

View graph