Comment by pron

BTW, this is the same approach taken by the Coq, Isabelle and Lean theorem provers. In all of them, 1/0 = 0. It is certainly unconventional, but whether this is wrong is a matter of philosophy. Basically, division by zero is undefined, but you can define it to be zero and so extend the definition. This is consistent with the rest of arithmetic. You get more theorems (like for all a, b and c, a/c = b/c), but no inconsistencies.