Simplified0.0
\[\leadsto \color{blue}{\frac{0.5}{y} - \frac{0.5}{x}}
\]
Proof
(-.f64 (/.f64 1/2 y) (/.f64 1/2 x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) y) (/.f64 1/2 x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (/.f64 (Rewrite<= *-inverses_binary64 (/.f64 x x)) 2) y) (/.f64 1/2 x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 x (*.f64 x 2))) y) (/.f64 1/2 x)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 x (*.f64 (*.f64 x 2) y))) (/.f64 1/2 x)): 69 points increase in error, 1 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (/.f64 (/.f64 (Rewrite<= *-inverses_binary64 (/.f64 x x)) 2) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 x x) (*.f64 2 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (/.f64 (/.f64 x x) (Rewrite<= *-commutative_binary64 (*.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (/.f64 (Rewrite=> *-inverses_binary64 1) (*.f64 x 2))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (/.f64 (Rewrite<= *-inverses_binary64 (/.f64 y y)) (*.f64 x 2))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 x (*.f64 (*.f64 x 2) y)) (Rewrite=> associate-/l/_binary64 (/.f64 y (*.f64 (*.f64 x 2) y)))): 49 points increase in error, 9 points decrease in error
(Rewrite<= div-sub_binary64 (/.f64 (-.f64 x y) (*.f64 (*.f64 x 2) y))): 1 points increase in error, 2 points decrease in error