https://github.com/leanprover/fp-lean/blob/272b8386a3501c7ec3286c94887ac398bcd70109/book/FPLean/GettingToKnow/Conveniences.lean#L425 `halven` -> `halve n`