proposition: Lemma null_sum_eq : forall A B C D, SumV A B B C D D -> A = C.
proof: Proof. intros. unfold SumV in H. assert(HH:= vector_construction B C B). ex_and HH D'. assert(HH:= (H D' H0)). assert(A = D'). apply (null_vector D). apply eqv_sym. apply HH. subst D'. apply vector_uniqueness in H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec