proposition: Lemma bezier_step_conv c n t : bezier c (S n) t = bezier (c \o S) n t <| t |> bezier c n t.
proof: Proof. by rewrite /= /conv addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection