Simplified0.0
\[\leadsto \color{blue}{\frac{y - x}{y + -1}}
\]
Proof
(/.f64 (-.f64 y x) (+.f64 y -1)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 y x) (+.f64 y (Rewrite<= metadata-eval (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 y x) (Rewrite<= sub-neg_binary64 (-.f64 y 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 y x) (-.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (-.f64 y x) (-.f64 y 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 y x)) (*.f64 -1 (-.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 y 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 y) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 y)) 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (Rewrite<= +-commutative_binary64 (+.f64 1 (neg.f64 y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 y x)) (Rewrite<= sub-neg_binary64 (-.f64 1 y))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 y x))) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 y x))) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 y) x)) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 y)) x) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 y))) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 x y)) (-.f64 1 y)): 0 points increase in error, 0 points decrease in error