A binary predicate $\text{\#}$ appearing in first-order intuitionistic logic that functions as a constructive counterpart to inequality in mathematics. In intuitionistic analysis, that $x_0$ and $x_1$ are unequal ($x_0\ne x_1$) means that the assumption that $x_0=x_1$ leads to a contradiction. That $x_0\text{\#}{x}_1$ asserts the existence of an effective means to calculate a positive, real-valued distance between $x_0$ and $x_1$, i.e., the existence of an algorithm calculating the value of $|x_0-x_1|$.