English
If n and d are positive numbers and q,r are numbers satisfying certain linear relations (h1,h2), then the divModAux operation yields quotient and remainder representing n with quotient q' and remainder r' such that n = r' + d·q' and r' < d.
Русский
Пусть n и d — положительные числа, q и r — числа, удовлетворяющие линейным условиям h1,h2. Тогда операция divModAux выдаёт конкурентное разложение n на частное q' и остаток r' с равенством n = r' + d·q' и r' < d.
LaTeX
$$$\forall n,d \in PosNum,\; \forall q,r \in Num,\; h_1:\ (r:\mathbb{N}) + d \cdot ((q:\mathbb{N}) + q) = n \land h_2:\ (r:\mathbb{N}) < 2d \Rightarrow \nexists\; (q',r'):\DivModAux(d,q,r) = (q',r') \,\text{ ofNat};\ (r' + d\cdot q') = n \land (r' : \mathbb{N}) < d$$$
Lean4
theorem divMod_to_nat_aux {n d : PosNum} {q r : Num} (h₁ : (r : ℕ) + d * ((q : ℕ) + q) = n) (h₂ : (r : ℕ) < 2 * d) :
((divModAux d q r).2 + d * (divModAux d q r).1 : ℕ) = ↑n ∧ ((divModAux d q r).2 : ℕ) < d :=
by
unfold divModAux
have : ∀ {r₂}, Num.ofZNum' (Num.sub' r (Num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d :=
by
intro r₂
apply Num.mem_ofZNum'.trans
rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
simp
rcases e : Num.ofZNum' (Num.sub' r (Num.pos d)) with - | r₂
· rw [Num.cast_bit0, two_mul]
refine ⟨h₁, lt_of_not_ge fun h => ?_⟩
obtain ⟨r₂, e'⟩ := Nat.le.dest h
rw [← Num.to_of_nat r₂, add_comm] at e'
cases e.symm.trans (this.2 e'.symm)
· have := this.1 e
simp only [Num.cast_bit1]
constructor
· rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
· rwa [this, two_mul, add_lt_add_iff_right] at h₂
