I think there is a mistake in the OCaml function and the mathematical definition in Task 9 of Exercise Sheet 13. The result for x < y should be (0, x) as 1\cdot y + x = x holds for y = 0 but the specification enforces y > 0. The C0 program, on the other hand, is correct.
Thank you. We will fix it.