To my understanding, at the beginning of a
payable function in a contract, an amount of
msg.value ether is added to the contract's balance.
Therefore, the expression
address(this).balance >= msg.value is always true.
Therefore, I can compute
address(this).balance - msg.value without any risk of underflow.
Is that correct?