Unicode "not equal" notation in Coq (≠)

Question

The following text is mentioned in SF book:

This is how we use not to state that 0 and 1 are different elements of nat:

Theorem zero_not_one : ~(0 = 1).
Proof.
  intros contra. inversion contra.
Qed.

Such inequality statements are frequent enough to warrant a special notation, x ≠ y:

Check (0 ≠ 1).
(* ===> Prop *)

But when I actually do this in Coq:

Check (0 ≠ 1).

It gives me this error:

Syntax Error: Lexer: Undefined token

In fact, looking at the standard library, I cannot seem to find any notation for that. So, what is the proper notation for it ?

Answer 1

As @jonathon said, the operator is written <>.

Check 1 <> 2.

But you can also do this:

Require Import Unicode.Utf8.
Check 1 ≠ 2.