Euclidean remainder of a negated dividend

Proved

burau_cf_emod_neg_of_pos

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

arithmeticcontinued-fractionseuclidean-algorithm

Euclidean remainder of a negated dividend. For positive integers $a,b$ ,

(-a)\bmod b = b\left\lceil \frac{a}{b}\right\rceil - a = b\cdot\frac{a+b-1}{b} - a,

the companion of the quotient formula $-a/b=-\lceil a/b\rceil$ . Together they give the one-step recursion of the standard Euclidean continued fraction of $-\frac1x$ in terms of that of $x$ , i.e. the negative reciprocal transformation of continued fractions.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem burau_cf_emod_neg_of_pos (a b : ℤ) (ha : 0 < a) (hb : 0 < b) :
    (-a) % b = b * ((a + b - 1) / b) - a := by sorry

Source

Euclidean algorithm on Z; cf. A. Ya. Khinchin, *Continued Fractions* (1964), Ch. II.

View graph