a little more line optimization

to_ccw_system.v

@@ -245,16 +245,14 @@ move/eqP/expand_ptb'/eqP; rewrite eq_sym => main.
 rewrite ptbd_value d00 add0r /exprz expr2 -mulrA -mulrDr mulf_eq0.
 rewrite polyX_eq0 /=; set p' := (X in X == _); suff vn0 : p'.[0] != 0.
   by apply/negP=>/eqP abs; case/negP: vn0; rewrite abs hornerE.
-rewrite /p' !hornerE; apply/negP=> /eqP abs; move: main; rewrite abs mulr0.
+rewrite /p' !hornerE; apply/negP=> /eqP A; move: main; rewrite A mulr0.
 have smn0 : (b.1 - a.1) ^ 2 + (b.2 - a.2) ^ 2 != 0.
   apply: lt0r_neq0; rewrite -(addr0 0) ltr_le_add // /exprz ?sqr_ge0 //.
   by rewrite exprn_even_gt0 /=.
-rewrite -!mulrA 2!mulf_eq0 (negbTE ba1n0) /= =>/orP[]; first by apply/negP.
-move=> it; move: it (step d00).
-by rewrite !(mulf_eq0, negbTE ba1n0) /= => /orP[] /eqP/subr0_eq ab';
-  rewrite ab' [in RHS]mulrBl (mulrC b.2) (addrAC (_ * b.2)) ?addrNK
-    ?addrN ?add0r ?(addrC (- _)) -?mulrBl -?mulrBr ?(mulrC _ (_ - _));
-  move=>/(mulfI ba1n0) ab2; move: uabc; rewrite /= !(uniq_rules, ab', ab2).
+rewrite -!mulrA !mulf_eq0 (negbTE ba1n0) (negbTE smn0) !subr_eq0 /= {A}.
+by move =>/orP[] /eqP A; move: (step d00) uabc; rewrite /= A (mulrBl _ b.2)
+  (mulrC b.2)(addrAC (_ * b.2)) ?addrNK ?addrN ?add0r ?(addrC (- _)) -?mulrBl
+  -?mulrBr ?(mulrC _ (_ - _))=>/(mulfI ba1n0) B; rewrite !(uniq_rules, A, B).
 Qed.
 
 Lemma non_zero_polynomial_interval :