Division_Theorem_v2
ProvedDivision algorithm: any integer can be divided by a nonzero integer with remainder.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Division_Theorem_v2 (a b : ℤ) (hb : b ≠ 0) : ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < |b| := by sorry