proposition: Lemma mkedgeE (a b : Plane R) (h : a.1 < b.1) : mkedge a b = Bedge h.
proof: Proof. rewrite /mkedge; case: (mkedge_aux a b)=> v Pv /=; apply: Pv. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection