Comment by bjt12345

I'm surprised to learn that lean defines the natural number 1/0 as 0.