I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.