proposition: Lemma bezier_bernstein2 c t : bezier c 2 t = \sum_(i < 3) (bernp 0 1 2 i).[t] *: c i.
proof: Proof. rewrite !big_ord_recr big_ord0 /= add0r. rewrite /= scalerDr scalerA -!addrA; congr (_ *: _ + _). by rewrite /bernp !hornerE /= subr0 expr1n invr1; ring. rewrite !(scalerA, scalerDr) addrA -scalerDl; congr (_ *:_ + _ *: _). by rewrite /bernp !hornerE /= subr0 expr1n invr1; ring. by rewrite /bernp !hornerE /= subr0 expr1n invr1; ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection