Simplified0.0
\[\leadsto \color{blue}{\left(m + -1\right) + \frac{m}{v} \cdot \left(1 + m \cdot -2\right)}
\]
Proof
(+.f64 (+.f64 m -1) (*.f64 (/.f64 m v) (+.f64 1 (*.f64 m -2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 -1 m)) (*.f64 (/.f64 m v) (+.f64 1 (*.f64 m -2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (*.f64 (/.f64 m v) (+.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 -2 m))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (/.f64 m v) 1) (*.f64 (/.f64 m v) (*.f64 -2 m))))): 4 points increase in error, 3 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (Rewrite=> *-rgt-identity_binary64 (/.f64 m v)) (*.f64 (/.f64 m v) (*.f64 -2 m)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (/.f64 m v) (*.f64 (/.f64 m v) (Rewrite=> *-commutative_binary64 (*.f64 m -2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (/.f64 m v) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 m v) m) -2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (/.f64 m v) (*.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 m m) v)) -2))): 4 points increase in error, 5 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (/.f64 m v) (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 m 2)) v) -2))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 -1 m) (+.f64 (/.f64 m v) (Rewrite<= *-commutative_binary64 (*.f64 -2 (/.f64 (pow.f64 m 2) v))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 -1 (+.f64 m (+.f64 (/.f64 m v) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))))): 0 points increase in error, 1 points decrease in error
(+.f64 -1 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 m (/.f64 m v)) (*.f64 -2 (/.f64 (pow.f64 m 2) v))))): 0 points increase in error, 0 points decrease in error
(+.f64 -1 (+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (/.f64 m v) m)) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))): 0 points increase in error, 0 points decrease in error
(+.f64 -1 (+.f64 (+.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 m)) v) m) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))): 0 points increase in error, 0 points decrease in error
(+.f64 -1 (+.f64 (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 v) m)) m) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))): 36 points increase in error, 2 points decrease in error
(+.f64 -1 (+.f64 (Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (/.f64 1 v) 1) m)) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))): 0 points increase in error, 0 points decrease in error
(+.f64 -1 (+.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (/.f64 1 v))) m) (*.f64 -2 (/.f64 (pow.f64 m 2) v)))): 0 points increase in error, 0 points decrease in error
(+.f64 -1 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -2 (/.f64 (pow.f64 m 2) v)) (*.f64 (+.f64 1 (/.f64 1 v)) m)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -2 (/.f64 (pow.f64 m 2) v)) (*.f64 (+.f64 1 (/.f64 1 v)) m)) -1)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -2 (/.f64 (pow.f64 m 2) v)) (*.f64 (+.f64 1 (/.f64 1 v)) m)) (Rewrite<= metadata-eval (neg.f64 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 (+.f64 (*.f64 -2 (/.f64 (pow.f64 m 2) v)) (*.f64 (+.f64 1 (/.f64 1 v)) m)) 1)): 0 points increase in error, 0 points decrease in error