proposition: Lemma ise_to_is : forall A B C D E F, SumV_exists A B C D E F -> SumV A B C D E F.
proof: Proof. intros. ex_and H D'. unfold SumV. intros. assert(D'= D'0). apply (vector_construction_uniqueness C D B). apply eqv_sym. apply H. assumption. subst D'0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec