Comment by Jensson

In programming the simplifications has to be correct even if you don't prove them, and being correct isn't that easy.