proposition: Lemma bezier2_dichotomy_l (c : nat -> Plane R) (t u : R) : bezier c 2 (t * u) = bezier (f3pt (c 0%nat) (bezier c 1 u) (bezier c 2 u)) 2 t.
proof: Proof. rewrite /bezier /= !scalerDr !scalerA !addrA. rewrite !(addrAC _ (_ *: c (S O)) (_ *: c O)) -!scalerDl. rewrite -!addrA; congr (_ *: _ + _); first by ring. 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