True, but I would want that reasoning to have some representation in the code as well, which doesn't happen if you do a proof to the side.