English
For all k ∈ ℕ⁺, r,q ∈ ℕ with not (r = 0 ∧ q = 0), the equation holds
Русский
Для всех k ∈ ℕ⁺, r,q ∈ ℕ, не выполняется (r = 0 ∧ q = 0), выполняется равенство
LaTeX
$$$$ \forall k \in \mathbb{N}_{>0},\; r,q \in \mathbb{N},\; \neg(r = 0 \land q = 0) \Rightarrow ((\text{modDivAux } k\ r\ q).1 : \mathbb{N}) + k \cdot (\text{modDivAux } k\ r\ q).2 = r + k \cdot q $$$$
Lean4
theorem mod_add_div (m k : ℕ+) : (mod m k + k * div m k : ℕ) = m :=
by
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)
have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) :=
by
rintro ⟨hr, hq⟩
rw [hr, hq, mul_zero, zero_add] at h₀
exact (m.ne_zero h₀.symm).elim
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
exact this.trans h₀
