fact: Fixpoint bezier (c : nat -> Plane R) (n : nat) (t : R) := match n with | 0 => c 0%N | S p => (1 - t) *: (bezier c p t) + t *: (bezier (c \o S) p t) end.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection