I am sorry I spoilt that, "x/x = 1 - 0/x" , reduces to "0 = 1 - 0", for x = 0 in Mizar, which really should not be provable. The message should be that due to such defaults, objects like the function x/x give sometimes rise to strange theorems. Best, Josef