lean_workbook_plus_33165

Proved

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

Prove that $2k \equiv n \mod 2k-n$ for all even numbers $k$ and $n$ such that $n \leq k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33165 (k n : ℕ) (h₁ : Even k) (h₂ : Even n) (h₃ : n ≤ k) : 2 * k ≡ n [ZMOD 2 * k - n]   :=  by sorry

Source