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