title: Unicode "not equal" notation in Coq (≠)
body: <p>The following text is mentioned in SF book:</p>
  
  <p>This is how we use not to state that 0 and 1 are different elements of nat:</p>
  
  <blockquote>
  <pre><code>Theorem zero_not_one : ~(0 = 1).
  Proof.
    intros contra. inversion contra.
  Qed.
  </code></pre>
    
    <p>Such inequality statements are frequent enough to warrant a special
    notation, x ≠ y:</p>
  
  <pre><code>Check (0 ≠ 1).
  (* ===&gt; Prop *)
  </code></pre>
  </blockquote>
  
  <p>But when I actually do this in Coq:</p>
  
  <pre><code>Check (0 ≠ 1).
  </code></pre>
  
  <p>It gives me this error:</p>
  
  <pre><code>Syntax Error: Lexer: Undefined token
  </code></pre>
  
  <p>In fact, looking at the <a href="https://coq.inria.fr/library/Coq.Init.Notations.html" rel="nofollow noreferrer">standard
  library</a>, I
  cannot seem to find any notation for that. So, what is the proper
  notation for it ?</p>