Symbol: Dbl_subtract_withextension