proposition: Lemma bezier2_dichotomy_r (c : nat -> Plane R) (t u : R) : bezier c 2 (u + t * (1 - u)) = bezier (f3pt (bezier c 2 u) (bezier (c \o S) 1 u) (c 2%nat)) 2 t.
proof: Proof. rewrite /bezier /= !scalerDr !scalerA !addrA. rewrite -!addrA; congr (_ *: _ + _); first by ring. rewrite !addrA -!scalerDl. rewrite !(addrAC _ (_ *: c (S (S _))) (_ *: c (S O))) -!scalerDl. rewrite -!addrA -!scalerDl. congr (_ *: _ + _ *: _); ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection