∀ {L : Type u_1} [inst : RightPreLieRing L] (x y z : L),
  associator x y z = associator x z y →
    associator z x y = associator z y x →
      associator y z x = associator y x z →
        associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y