Division_Theorem_Positive_Divisor
ProvedFor any integers a, b with b ≠ 0, there exist unique q, r such that a = qb + r with 0 ≤ r < |b|.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Division_Theorem_Positive_Divisor (a b : ℤ) (hb : b ≠ 0) : ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < Int.natAbs b := by sorry