proposition: Lemma bezier1_conv c t : bezier c 1 t = c 0%nat <| (1 - t) |> c 1%nat.
proof: Proof. rewrite /= /conv; congr (_ *: _ + _ *: _); ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection