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. Based on df-sub . (Contributed by Steven Nguyen, 7-Jan-2022)