proposition: Lemma conv_p1 (a b : Plane R) t : (a <| t |> b).1 = ((a.1 : R^o) <| t |> b.1).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection