fact: Definition f3pt (a b c : Plane R) := [fun n : nat => a with 1%nat |-> b, 2%nat |-> c].
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection