proposition: Lemma safe_bezier_ccw_corner_side (a b c : Plane R) (v : vert_edge) (u : R): ccw a b c -> a.1 < b.1 < c.1 -> a.1 < ve_x v < c.1 -> on_vert_edge b v -> u \in `]0, 1[ -> (bezier (f3pt a b c) 2 u).1 = ve_x v -> ve_bot v < (bezier (f3pt a b c) 2 u).2.
proof: Proof. move=> abc abc1 avc bon uin bzx. move: (bon) => /andP[] /eqP bx /andP[]bl bh. apply: (lt_trans bl). rewrite -subr_gt0. have abb : det a b b = 0. by rewrite det_cyclique det_alternate. have bzxb : b.1 = (bezier (f3pt a b c) 2 u).1 by rewrite bzx. rewrite (height_bezier2 abc1 abb bzxb). apply: divr_gt0; last by lra. apply: mulr_gt0; last by []. rewrite in_itv /= in uin. have tmp : 0 < u < 1 by exact uin. apply: mulr_gt0; lra. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection