Simplified26.7
\[\leadsto \color{blue}{\frac{y}{a} - \frac{x}{z \cdot a}}
\]
Proof
(-.f64 (/.f64 y a) (/.f64 x (*.f64 z a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y (Rewrite<= /-rgt-identity_binary64 (/.f64 a 1))) (/.f64 x (*.f64 z a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y (/.f64 a (Rewrite<= *-inverses_binary64 (/.f64 z z)))) (/.f64 x (*.f64 z a))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a z) z))) (/.f64 x (*.f64 z a))): 25 points increase in error, 1 points decrease in error
(-.f64 (/.f64 y (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 z a)) z)) (/.f64 x (*.f64 z a))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y z) (*.f64 z a))) (/.f64 x (*.f64 z a))): 48 points increase in error, 4 points decrease in error
(Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 y z) x) (*.f64 z a))): 2 points increase in error, 2 points decrease in error
(/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 y z) (neg.f64 x))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 y z)))) (neg.f64 x)) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (neg.f64 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 y (neg.f64 z)))) (neg.f64 x)) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 y (neg.f64 z)))) (neg.f64 x)) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 (*.f64 y (neg.f64 z))) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 -1 (+.f64 (*.f64 y (neg.f64 z)) x))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 y (neg.f64 z))))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (+.f64 x (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 y z))))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (Rewrite<= sub-neg_binary64 (-.f64 x (*.f64 y z)))) (*.f64 z a)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (-.f64 x (*.f64 y z))) (Rewrite=> *-commutative_binary64 (*.f64 a z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x (*.f64 y z)) (*.f64 a z)))): 0 points increase in error, 0 points decrease in error