[contravariant]

Hmm, I think there also needs to be a rule that you can't have a numerator of 0, otherwise any case where you have an expression a * b = 0 with a = 0 then either b=0 or a / b = 0. So the restriction that you can't multiply by 0 becomes somewhat meaningless.

[zmonx]

The constraints I impose are sufficient to exclude such cases in multiplications: a/b is first evaluated, and if the result is 0, it is precluded from multiplications. To avoid also divisions resulting in 0, you are right: We can easily constrain the nominator to express this, completely analogously to multiplication. This goes beyond the initial requirements though.