I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e.

It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort.

Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.