Theoretical computer science or combinatorics or algorithmics: The diamond lemma.
Some days ago, while giving a seminar talk about Clifford algebras, I realized that Lawson-Michelson has a flawed proof that the canonical inclusion of a vector space in its own Clifford algebra is indeed injective (unfortunately, not until I had written this proof on desk). Most other literature gives ugly proofs using orthogonalization. Fact is, this injectivity works in a much more general context (namely, it works for any module over a commutative ring with $1$), where of course there needs not be any orthogonalization. And it is easily proven using the diamond lemma. A similar assertion for Weyl algebras is also clear from the diamond lemma, and so is the Poincaré-Birkhoff-Witt theorem (which is proven in intricate and opaque ways in most of literature). Maybe the problem is that geometers don't know enough computer science?
