Division_Theorem
Proveddivision-theoremdivisorsnamed-theoremsproofwiki
For every pair of integers a, b where b ≠ 0, there exist unique integers q, r such that a = qb + r and 0 ≤ r < |b|.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Division_Theorem (a b : ℤ) (hb : b ≠ 0) : ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < Int.natAbs b := by sorry
Source