proposition: Lemma sum_exists : forall A B C D, exists E, exists F, SumV A B C D E F.
proof: Proof. intros. assert(HH:= vector_construction C D B). ex_and HH F. exists A. exists F. unfold SumV. intros. assert(D' = F). apply (vector_construction_uniqueness C D B); auto. subst D'. apply eqv_refl. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec