What <> is in Coq

Link:: https://stackoverflow.com/q/54938298

Display all goals and responses

Question

It's difficult to search for but wondering what <> means as in here:

Axiom point : Type.
Axiom line : Type.
Axiom lies_in : point -> line -> Prop.
Axiom ax : forall (p1 p2 : point),
    p1 <> p2 -> exists! l : line, lies_in p1 l /\ lies_in p2 l.

Answer

x <> y is a notation for ~(x = y) (which itself is a notation for (x = y) -> False). It's possible to search for notations with the Locate vernacular command, which is used like Locate "<>". and gives output like

Notation "x <> y  :> T" := (not (eq x y)) : type_scope
  (default interpretation)
Notation "x <> y" := (not (eq x y)) : type_scope
  (default interpretation)