Ah, thanks for the link. I suggested the reason that Isabelle/HOL does this is because it requires total functions and you don't have a convenient way to do refinement types. But that's not an adequate explanation, because Lean does allow such refinements, but it still turns out to be inconvenient for division.
I will note that setting a - b = 0 for a <= b is pretty standard, and is often called "partial subtraction."
Comments
Ah, thanks for the link. I suggested the reason that Isabelle/HOL does this is because it requires total functions and you don't have a convenient way to do refinement types. But that's not an adequate explanation, because Lean does allow such refinements, but it still turns out to be inconvenient for division.
I will note that setting a - b = 0 for a <= b is pretty standard, and is often called "partial subtraction."