Broken div example proof chapter 8

[ketilwright]

This example generates errors

example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by
  conv => lhs; unfold div -- unfold occurrence in the left-hand-side of the equation

In spite of the text saying "the defining example for div does not hold definitionally. . ", I was able to rw [div]; rfl

example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by
  rw [div]; rfl
  

lean --version
Lean (version 4.12.0, x86_64-apple-darwin22.6.0, commit dc2533473114, Release)