A much simpler proof of Knuth's 4th axiom thanks to tail_coefD_gt0

to_ccw_system.v

@@ -631,6 +631,24 @@ rewrite -lerNgt ler_eqVlt tail_coef_eq0 (negbTE ptbn0) /= tail_coefN oppr_gt0.
 by right.
 Qed.
 
+Lemma Kn4 (R : realDomainType) (a b c d : R * R) :
+  ccw a b d -> ccw b c d -> ccw c a d -> ccw a b c.
+Proof.
+move=> abd bcd cad.
+set uabd := ccw_uniq abd.
+set ubcd := ccw_uniq bcd.
+set ucad := ccw_uniq cad.
+have uabc : uniq [:: a; b; c].
+  move: (uabd) (ubcd) (ucad); rewrite /= !(inE, negb_or) -!andbA (eq_sym a c).
+  by move=> /andP[] -> _ /andP[] -> _ /andP[] -> _.
+rewrite ccw_tail_coef //.
+have -> : ptbs a b c = ptbs b c d + ptbs c a d + ptbs a b d.
+  have := Knuth_4_main (ptb a) (ptb b) (ptb c) (ptb d).
+  rewrite -/(ptbs a b c) -/(ptbs a b d) -/(ptbs b c d) swap_det_surface.
+  by rewrite -/(ptbs c a d) opprK => /eqP; rewrite subr_eq0 eq_sym => /eqP.
+by rewrite !tail_coefD_gt0 // -ccw_tail_coef.
+Qed.
+
 Definition bnd (R : realFieldType) (a b c : R * R) (h : uniq [::a; b; c]) : R :=
   proj1_sig
     (non_zero_polynomial_sign (non_zero_polynomial h)).
@@ -660,40 +678,6 @@ case:ifP; case: ifP=> _ _ _ /eqP; rewrite ?(negbTE (oner_neq0 R)) ?znm1 //;
 by case:ifP=> _ //; rewrite ?(eq_sym (1 : R)) (negbTE m1not1).
 Qed.
 
-Lemma Kn4 (R : realFieldType) (a b c d : R * R) :
-  ccw a b d -> ccw b c d -> ccw c a d -> ccw a b c.
-Proof.
-move=> abd bcd cad.
-set uabd := ccw_uniq abd.
-set ubcd := ccw_uniq bcd.
-set ucad := ccw_uniq cad.
-have uabc : uniq [:: a; b; c].
-  move: (uabd) (ubcd) (ucad); rewrite /= !(inE, negb_or) -!andbA (eq_sym a c).
-  by move=> /andP[] -> _ /andP[] -> _ /andP[] -> _.
-set epsilon := Num.min (bnd uabd)
-  (Num.min (bnd ubcd) (Num.min (bnd ucad) (Num.min (bnd uabc) 1))).
-have egt0 : 0 < epsilon by rewrite !ltr_minr !bnd0 ltr01.
-set t := epsilon/2%:R; have /andP [tgt0 tlte] : 0 < t < epsilon.
-  by have := midf_lt egt0; rewrite add0r => [][-> ->].
-have tabd : 0 < t < bnd (uabd).
-  by rewrite tgt0 /= (ltr_le_trans tlte) // !ler_minl lerr ?orbT.
-have tbcd : 0 < t < bnd (ubcd).
-  by rewrite tgt0 /= (ltr_le_trans tlte) // !ler_minl lerr ?orbT.
-have tcad : 0 < t < bnd (ucad).
-  by rewrite tgt0 /= (ltr_le_trans tlte) // !ler_minl lerr ?orbT.
-have tabc : 0 < t < bnd (uabc).
-  by rewrite tgt0 /= (ltr_le_trans tlte) // !ler_minl lerr ?orbT.
-move: (abd); rewrite (ccw_to_ptb tabd).
-move: (bcd); rewrite (ccw_to_ptb tbcd).
-move: (cad); rewrite (ccw_to_ptb tcad)=> pcad pbcd pabd.
-rewrite (ccw_to_ptb tabc).
-have vabc : ptbs a b c = ptbs b c d + ptbs c a d + ptbs a b d.
-  have := Knuth_4_main (ptb a) (ptb b) (ptb c) (ptb d).
-  rewrite -/(ptbs a b c) -/(ptbs a b d) -/(ptbs b c d) swap_det_surface.
-  by rewrite -/(ptbs c a d) opprK => /eqP; rewrite subr_eq0 eq_sym => /eqP.
-by rewrite vabc -horner_evalE !rmorphD /= !horner_evalE !addr_gt0.
-Qed.
-
 Lemma Kn5 (R : realFieldType) (a b c d e : R * R):
   ccw a b c -> ccw a b d -> ccw a b e ->
   ccw a c d -> ccw a d e -> ccw a c e.