I'm working my way through Bird's _Introduction to Functional Programming Using Haskell_. I'd appreciate any help with problem 3.3.3, which is:

"Division of natural numbers can be specified by the condition (n * m) / n = m for all positive n and all m. Construct a program for division and prove that it meets the specification."

The required construction relies on the following definitions:

data Nat = Zero| Succ Nat

(+) :: Nat -> Nat

m + Zero = m

m + Succ n = Succ (m + n)

(*) :: Nat -> Nat

m * Zero = Zero

m * Succ n = m * n + m

Proceeding as Bird does in Sec. 3.2.2, where he derives the definition of "-" from the specification "(m + n) - n = m", I've so far gotten the first case, in which m matches the pattern "Zero", simply by (i) substituting Zero for m in the specification, (ii) substituting Succ n for n in the specification (solely because n is constrained to be positive), and (iii) reducing by applying the first equation of "*":

Case Zero:

(Succ n * Zero) / Succ n = Zero

≡ {first equation of "*"}

Zero / Succ n = Zero

Easy enough, and completely intuitive, since we expect Zero divided by any non-Zero finite number to be Zero. The next case, in which m matches the pattern "Succ m", is where I get stuck, and I really have no intuition about what the definition is supposed to be. My first step is to substitute "Succ m" for "m" in the given specification, and to substitute Succ n for n in the specification (for the same reason, as above, that n is constrained to be positive), and then to use the definition of "*" to reduce the equation:

Case Succ m:

Succ n * Succ m / Succ n = Succ m

≡ {second equation of "*"}

(Succ n * m + Succ n) / Succ n = Succ m

Where do I go from here? Thank you so much.