Thoses examples you linked are different, they incorrectly assume that slice[:i] should prove slice[i:].
This is wrong because go use [x,y) ranging, that means :i is one past the index that will be taken, while i: is the last index that will be taken. In other words i <= cap(slice) does not prove i < cap(slice).
Here we have a different issue, actually it reproduce just like this without this double left / right reslicing:
In other words feeding an empty slice produce two empty slices.
This was easy to fix, I just had to teach the compiler that for unsigned divisions z := x / y and unsigned right shifts (which are really just divisions by powers of two) z := x >> y, z is always smaller or equal to x.