proposition: Lemma eqv_mid : forall A B C, EqV A B B C -> Midpoint B A C.
proof: Proof. intros. unfold EqV in H. induction H. apply plg_mid in H. ex_and H M. apply l7_3 in H0. subst M. assumption. spliter. subst C. subst B. apply l7_3_2. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec