proposition: Lemma null_sum : forall A B C, SumV A B B A C C.
proof: Proof. intros. unfold SumV. intros D H. assert(A = D). apply (vector_uniqueness B). apply H. subst D. apply eqv_trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec