proposition: Lemma null_vector : forall A B C, EqV A A B 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 H. Col. apply plgf_trivial_neq in H. spliter. subst C. tauto. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec