proposition: Lemma is_to_ise : forall A B C D E F, SumV A B C D E F -> SumV_exists A B C D E F.
proof: Proof. intros. unfold SumV in H. unfold SumV_exists. assert(HH:= (vector_construction C D B)). ex_and HH D'. assert(HH:=(H D' H0)). exists D'. split. apply eqv_sym. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec