proposition: Lemma vector_construction : forall A B C, exists D, EqV A B C D.
proof: Proof. intros. induction (eq_dec_points A B). exists C. right. tauto. assert(HH:= midpoint_existence B C). ex_and HH M. prolong A M D A M. exists D. left. apply (mid_plg _ _ _ _ M). induction(eq_dec_points A D). subst D. right. intro. subst C. apply l7_3 in H0. apply between_identity in H1. subst M. contradiction. left. assumption. split; Cong. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec