Feature Request: Not Equals Zero Component

[NoamDev]

It'd be cool to have a not equals component that would be more efficient that compare component or packing component + disjunction component. The constraint I suggest is: inv * x =1 for some inv. This can only be true if x is non zero. on witness generation inv would be assigned the inverse of x. It'd better to write it in a way that supports linear combinations and not just variables, this way it could be used to check that any two numbers/variables are different just by subtracting one from the other and using the not_zero component on the linear combination.