proposition: Lemma safe_bezier_ccw (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 -> ~~((ve_x v, ve_top v) <<= mkedge a c) -> 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 -> on_vert_edge (bezier (f3pt a b c) 2 u) v.
proof: Proof. move=> abc bint vint topP uin /[dup] bzx /eqP bzxb bzb. rewrite /on_vert_edge bzxb bzb 2!andTb. have ac_cond : a.1 < c.1 by lra. have vav : valid_edge (mkedge a c) (ve_x v, ve_top v). rewrite/valid_edge mkedgeE [(left_pt _).1]/= [(right_pt _).1]/=. by rewrite ?ltW //; move: vint=> /andP[]. move: topP. rewrite (under_proj vav) -ltNge; apply le_lt_trans. rewrite (_ : (ve_x v, ve_top v).1 = (bezier (f3pt a b c) 2 u).1); last first. by rewrite bzx. rewrite -under_proj; last by rewrite /valid_edge bzx; exact: vav. rewrite /point_under_edge. rewrite bezier_step_conv. have vacp : valid_edge (mkedge a c) (bezier (f3pt a b c) 2 u). rewrite/valid_edge mkedgeE [(left_pt _).1]/= [(right_pt _).1]/= bzx. by rewrite ?ltW //; move: vint=> /andP[]. rewrite det_conv -sgz_le0. have Cuin : 0 < 1 - u < 1 by rewrite in_itv /= in uin; lra. set X := (X in X <= 0). suff : X = -1. by move=> ->; apply: lerN10. rewrite {}/X. apply: conv_num_sg=> //. apply: ltr0_sgz. rewrite bezier_step_conv det_conv. rewrite convC. apply: conv_num_ltr=> //. rewrite /=; move: abc; rewrite /ccw mkedgeE /= => abc. by rewrite det_inverse oppr_lte0 -det_cyclique. by rewrite /= mkedgeE /= -det_cyclique det_alternate. apply: ltr0_sgz. rewrite bezier_step_conv det_conv. apply: conv_num_ltr=> //. rewrite /=; move: abc; rewrite /ccw mkedgeE /= => abc. by rewrite det_inverse oppr_lte0 -det_cyclique. by rewrite mkedgeE /= det_alternate. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection