English
Let k be a positive natural number and r, q be natural numbers not both zero. If (m, t) = modDivAux(k, r, q), then m + k·t = r + k·q.
Русский
Пусть k ∈ ℕ_{>0} и r, q ∈ ℕ не одновременно равны нулю. Пусть (m, t) = modDivAux(k, r, q). Тогда m + k·t = r + k·q.
LaTeX
$$$\\pi_1(\\operatorname{modDivAux}(k,r,q)) + k \\cdot \\pi_2(\\operatorname{modDivAux}(k,r,q)) = r + k q$$$
Lean4
/-- Lemmas with div, dvd and mod operations -/
theorem modDivAux_spec :
∀ (k : ℕ+) (r q : ℕ) (_ : ¬(r = 0 ∧ q = 0)), ((modDivAux k r q).1 : ℕ) + k * (modDivAux k r q).2 = r + k * q
| _, 0, 0, h => (h ⟨rfl, rfl⟩).elim
| k, 0, q + 1, _ => by
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
| _, _ + 1, _, _ => rfl
