fact: Definition strict_inside_closed (p : Plane R) (c : cell) := (p <<< high c) && (~~(p <<= low c)) && (left_limit c < p.1 < right_limit c).
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection