proposition: Lemma mid_eqv : forall A B C, Midpoint A B C -> EqV B A A C.
proof: Proof. intros. unfold EqV. induction(eq_dec_points A B). subst B. apply is_midpoint_id in H. subst C. right. tauto. left. apply (mid_plg _ _ _ _ A). left. intro. subst C. apply l7_3 in H. contradiction. assumption. Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec