  When improving results about generalized inverses, the aim often is to do
this in the most general setting possible by eliminating superfluous
assumptions and by simplifying some of the conditions in statements. In this
paper, we use Hartwig's well-known triple reverse order law as an example for
showing how this can be done using a recent framework for algebraic proofs and
the software package OperatorGB. Our improvements of Hartwig's result are
proven in rings with involution and we discuss computer-assisted proofs that
show these results in other settings based on the framework and a single
computation with noncommutative polynomials.
