able to use `zero_mul` to prove itself

[haifron]

I found this by accident in the middle of proving zero_mul, and have tried on a new session and it works, as shown in the below screenshot.

when I was proving it in my initial attempt I did at least get an error, though it didn't prevent the proof from continuing:

[joneugster]

The initial error reported here should now be (partially) fixed:

• on "regular" it yields an error
• on "relaxed" it yields a warning

However, there is an underlying problem that needs to be addressed here. I'm going to open an issue explaining this on the lean4game-repo, as I don't have a trivial solution in mind: lean4game#117