Can I in Coq define a class with a notation for its field such that another field uses the notation?

Question

It's basically this question but about classes.

Imagine I want to do this:

Class CMonoid :=
  { A : Type
  ; operator : A -> A -> A
  ; property : a <> b = b <> a (* note the use of <> *)
  ; ...
  }

Notation "a <> b" := operator a b. (* too late! *)

Where can I insert the notation definition so I can write the above?

This may look like an overkill for notation, but that's because it's a simplified example. The real use case is a very long definition, and I want to use notation to simplify it.

Answer 1

This seems to work:

Reserved Notation "a <> b"
  (at level 70, no associativity).

Class CMonoid :=
  { A : Type
  ; operator : A -> A -> A
      where "a <> b" := (operator a b)
  ; property : forall (a b : A),
      (a <> b) = (b <> a)
  }.

Source: https://github.com/coq/coq/issues/7187