proposition: Lemma vector_uniqueness : forall A B C, EqV A B A C -> B = C.
proof: Proof. intros. unfold EqV in H. induction H. induction H. induction H. unfold TS in H. spliter. apply False_ind. apply H2. Col. apply plgf_permut in H. apply plgf_sym in H. apply (plgf_trivial_neq A B C ). assumption. spliter. subst A. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec