proposition: Lemma vert_edge_eqP : Equality.axiom vert_edge_eqb.
proof: Proof. move=> [vxa vta vba] [vxb vtb vbb] /=. have [/eqP <-|/eqP anb] := boolP(vxa == vxb). have [/eqP <-|/eqP anb] := boolP(vta == vtb). have [/eqP <-| /eqP anb] := boolP(vba == vbb). by apply:ReflectT. by apply: ReflectF=> [] []. by apply: ReflectF=> [] []. by apply: ReflectF=> [] []. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection