Facts involving constants don't propagate to bounds checks about wuffs HOT 4 CLOSED

git clone https://github.com/mvdan/zstd
git checkout tmp-break-inv
./build

check: cannot prove "i <= 131072": cannot prove "block_size <= 131072": failed at decode.wuffs:86. Facts:
        max_block_size == 131072
        block_size <= max_block_size
        i < block_size

var i u32
while i < block_size,
        inv max_block_size == 131072,
        inv block_size <= max_block_size {
        assert i <= max_block_size via "a <= b: a <= c; c <= b"(c:block_size)
        i += 1
}