English
Natural division is primitive recursive.
Русский
Деление на натуральные числа примитивно вычисимо.
LaTeX
$$$\\text{nat\_div}: \\mathbb{N}\\times\\mathbb{N}\\to\\mathbb{N}$ is primitive recursive.$$
Lean4
theorem nat_div : Primrec₂ ((· / ·) : ℕ → ℕ → ℕ) :=
by
refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_
have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨ (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
PrimrecPred.or (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
(.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
.and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
(nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))
refine this.of_eq ?_
rintro ⟨a, k⟩ q
if H : k = 0 then simp [H, eq_comm]
else
have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
simpa [H, zero_lt_iff, eq_comm (b := q)]
