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.