lean_workbook_plus_43714

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that for any natural $n$ , there are nonnegative integers $q, r$ such that $0 \le r < 3$ and $n = 3q + r$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43714 (n : ℕ) : ∃ q r : ℕ, 0 ≤ r ∧ r < 3 ∧ n = 3 * q + r   :=  by sorry

Source