English
For positive numbers d and n, the division n/d and the remainder n mod d, when viewed as natural numbers, correspond to the first and second components of divMod d n respectively.
Русский
Пусть d и n положительны. Непосредственно деление n/d и остаток n mod d, рассмотренные как натуральные числа, совпадают с первыми и вторыми компонентами пары divMod d n соответственно.
LaTeX
$$$\forall d,n \in PosNum,\ (n/d : \mathbb{N}) = (divMod\ d\ n).1 \land (n \% d : \mathbb{N}) = (divMod\ d\ n).2$$$
Lean4
theorem divMod_to_nat (d n : PosNum) : (n / d : ℕ) = (divMod d n).1 ∧ (n % d : ℕ) = (divMod d n).2 :=
by
rw [Nat.div_mod_unique (PosNum.cast_pos _)]
induction n with
| one => exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
| bit1 n IH =>
unfold divMod
revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
simp only at IH ⊢
apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
· rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
· omega
| bit0 n IH =>
unfold divMod
revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
simp only at IH ⊢
apply divMod_to_nat_aux
· simp only [Num.cast_bit0, cast_bit0]
rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
· simpa using IH.2
