proposition: Lemma detDM3 (l p1 p2 q1 q2 r1 r2 : R) : det (p1, p2) (q1, q2) (r1, r2) = det (p1, p2) (q1, q2) (r1 + l * (q1 - p1), r2 + l * (q2 - p2)).
proof: Proof. by rewrite !develop_det /xcoord /ycoord /=; ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection