Description: "Minus times minus is plus", see also nnmtmip , holds for positive
reals, too (formalized to "The product of two negative reals is a positive
real"). "The reason for this" in this case is that ( -u A x. -u B )= ( A x. B ) for all complex numbers A and B because of
mul2neg , A and B are complex numbers because of rpcn , and
( A x. B ) e. RR+ because of rpmulcl . Note that the opposites
-u A and -u B of the positive reals A and B are negative
reals. (Contributed by AV, 23-Dec-2022)