As the title indicates, I am seeking some perspective (explained below) on Bergman's Diamond Lemma.

I know that it can be used, for instance, to prove the Poincare-Birkhoff-Witt theorem for universal enveloping algebras. This is shown in Bergman's original paper. And then it can be used also for quantized enveloping algebras, quantized function algebras, etc.

I am also aware of this page at Secret Blogging Seminar, which discusses the Diamond Lemma in the graph-theoretic setting. It is stated there that this version can be used to prove the Jordan-Holder theorem on composition series for a finite group (and presumably for modules over a ring, etc).

For this to be a well-formulated question, I need to make clear what I mean by "perspective". Here is a quote from the introduction to the paper:

The main results in this paper are trivial. But what is trivial when described in the abstract can be far from clear in the context of a complicated situation where it is needed.

And then, later, after describing the results, he says:

This fact has been considered obvious and used freely by some ring-theorists (e.g., [17, Sect. !5l), but others seem unaware of it and write out tortuous verifications.

So, what I am looking for is examples of situations where the formalism of the Diamond Lemma really clarified or simplified some algebraic construction, or examples of people writing out "tortuous verifications" when they could have appealed to the Diamond Lemma instead.

PS If you've never looked at Bergman's paper before, you should! It's one of my favorites. Everything is so clear and well-motivated. If only I could write like that...