fact: Fixpoint check_bezier_ccw (fuel : nat) (v : vert_edge) (a b c : Plane R) : option bool := match fuel with | O => None | S p => let top_edge := (ve_x v, ve_top v) in if negb (point_under_edge top_edge (mkedge a c)) then Some true else if point_under_edge top_edge (mkedge a b) || point_under_edge top_edge (mkedge b c) then Some false else let b' := midpoint a b in let b2 := midpoint b c in let c' := midpoint b' b2 in if c'.1 < ve_x v then check_bezier_ccw p v c' b2 c else if ve_x v < c'.1 then check_bezier_ccw p v a b' c' else if c'.2 < ve_top v then Some true else Some false end.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection