proposition: Lemma mid_plgs : forall A B C D M, ~ Col A B C -> Midpoint M A C -> Midpoint M B D -> Parallelogram_strict A B C D.
proof: Proof. intros. unfold Parallelogram_strict. assert(A <>C). intro. apply H. subst C. Col. assert(B <> D). intro. subst D. apply l7_3 in H1. subst M. unfold Midpoint in H0. spliter. apply bet_col in H0. contradiction. assert(M <> D). intro. subst M. apply l7_2 in H1. apply is_midpoint_id in H1. subst D. tauto. assert( M <> A). intro. subst M. apply is_midpoint_id in H0. contradiction. repeat split. intro. apply H. Col. intro. unfold Midpoint in *. spliter. apply bet_col in H0. apply bet_col in H1. apply H. assert(Col M A D). ColR. assert(Col M A B). ColR. ColR. exists M. unfold Midpoint in *. spliter. split. apply bet_col in H0. Col. apply H1. apply (l12_17 _ _ _ _ M). intro. subst B. apply H. Col. assumption. assumption. eapply (l7_13 M); Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel