Example 37.1 Suppose you are working with matrices a,b,c etc. If an NCProcess command discovers that ab = bc and, at that point, you realize that it is reasonable to assume that no eigenvalue of a is an eigenvalue of c, then b must be zero from an analytic argument.¹ Therefore, one can add the polynomial equation b = 0 to the collection of polynomial equations and continue. As research progressed, one would add more and more analytic observations at the points where it became clear what those observations were.

Fact 37.2 If 〈 whatever hypothesis 〉, then ab = bc.

Fact 37.3 If a, b and c are matrices, no eigenvalue of a is an eigenvalue of c and ab = bc, then b = 0.

Fact 37.4 If 〈 whatever hypothesis 〉 and b = 0, then 〈 desired conclusion 〉.

Conclusion 37.5 If 〈 whatever hypothesis 〉, then 〈 desired conclusion 〉.