Formalization and verification of a circuit
for asserting that two booleans are not equal.
Given two field elements x and y representing booleans
(i.e. such that each field element is either 0 or 1;
see boolean-assert),
we combine the boolean-neq and boolean-assert-true
to constrain x and y to be non-equal: