[mason55]

You could prove to the type checker that you're only allowing input values that, when fed to your operation, results in outputs that remain in bounds. For example, if you're doing addition, you first check that each input is between 1 and 49, and you exhaustively handle the cases where the values are out of those bounds. Then the type checker can see that the output is always between 1 and 100.

For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"