> 3 and 4 are tedious, since you always need to prove that the inputs are nonzero.
Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.
As the article mentions, it doesn't necessarily work this way in a verified proof. Every time you form an expression involving division, you have to supply the proof. It is this repeated supplying of a proof (not necessarily having to reprove it) that is omitted in regular informal proofs that is tedious. In certain situations you can write automation to help you with that. But more frequently, you already have automation for other aspects of your proof, and this need to prove this is tripping up your other automation.
Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.