English
A version of the division algorithm with remainder for integers that allows negative divisors: the pair (q,r) representing a/b and a mod b is unique subject to r+bq = a and 0 ≤ r < |b|.
Русский
Версия алгоритма деления с остатком для целых чисел с отрицательными делителями: пара (q,r) уникальна при условиях r + bq = a и 0 ≤ r < |b|.
LaTeX
$$$\forall a,b,r,q \in \mathbb{Z},\ b \neq 0 \Rightarrow (a/b=q \land a\%b=r) \iff (r+bq=a \land 0 \le r \land r < |b|)$$$
Lean4
/-- Like `Int.ediv_emod_unique`, but permitting negative `b`. -/
theorem ediv_emod_unique'' {a b r q : Int} (h : b ≠ 0) : a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b| :=
by
constructor
· intro ⟨rfl, rfl⟩
exact ⟨emod_add_mul_ediv a b, emod_nonneg _ h, emod_lt_abs _ h⟩
· intro ⟨rfl, hz, hb⟩
constructor
· rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
simp
· rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]
