Description: Define subtraction between real numbers. This operator saves a few
axioms over df-sub in certain situations. Theorem resubval shows
its value, resubadd relates it to addition, and rersubcl proves its
closure. It is the restriction of df-sub to the reals: subresre .
(Contributed by Steven Nguyen, 7-Jan-2023)