proposition: Lemma vector_construction_uniqueness : forall A B C D D', EqV A B C D -> EqV A B C D' -> D = D'.
proof: Proof. intros. unfold EqV in *. induction H; induction H0. apply plg_comm2 in H. apply plg_comm2 in H0. apply (plg_uniqueness B A C); auto. spliter. subst B. subst D'. induction H. induction H. unfold TS in H. spliter. apply False_ind. apply H. Col. apply (plgf_trivial_neq A D C ). assumption. spliter. subst B. subst D. induction H0. induction H. unfold TS in H. spliter. apply False_ind. apply H. Col. apply plgf_comm2 in H. apply (plgf_trivial_neq A C D'). assumption. spliter. subst C. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec