diff --git a/to_ccw_system.v b/to_ccw_system.v index 847575af014033bdf6f04ea653e75268a92914fc..e9d0f021772c25f6a2f458d3e87eecc66a38199e 100644 --- a/to_ccw_system.v +++ b/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 :