Lemma in_vertex_set : forall p A B C,
    is_true (p \in (vertex_set (vertices_to_triangle A B C)))
          -> (p == A \/ p==B \/ p == C).
Proof.
move => p A B C p_vert.
pose z:=(vertices_to_triangle_correct A B C);move:z=>[vert_a [vert_b vert_c]].
by move:p_vert=> /imfsetP [[[|[|[|x']]] px] _] p_vert //=;
[left|right;left|right;right ];rewrite eq_sym;
apply/eqP;[rewrite vert_a|rewrite vert_b|rewrite vert_c];rewrite p_vert;
congr ((vertex (vertices_to_triangle A B C)) _ );apply ord_inj.
Qed.