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