proposition: Lemma detVert (p1 p2 q1 q2 r2 : R) : det (p1, p2) (q1, q2) (q1, r2) = (r2 - q2) * (q1 - p1).
proof: Proof. 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