nLab
denial inequality

The denial inequality is the negation of equality.

This is a term found in constructive mathematics, to distinguish from other inequality relations such as apartness. It is taken for granted in classical mathematics.

If one wishes to reserve the word “inequality” for order relations (such as $\le$ and $\lt$), then one may instead use the word disequality to refer to the denial inequality. (For instance, this is common in type theory with subtype? relations that form an ordering on the types.)