That's where more advanced type systems shine. You get to encode things like "this number is not null" and a safe division function will only take "not nulls" as the input.

The workflow would then be:

    1. prove that the input is not null (if input == 0) yielding a "not null number"
    2. running your calculation (no check needed for multiplication or division, if you add something you have to reprove that the number is not null)