This invariant holds for both the free and reserved balances. Document it. I also reformatted the documentation slightly.