proposition: Lemma mid_plgf : forall A B C D M, (A <> C \/ B <> D ) -> Col A B C -> Midpoint M A C -> Midpoint M B D -> Parallelogram_flat A B C D.
proof: Proof. intros. induction H. eapply (mid_plgf_aux A B C D M); assumption. apply plgf_sym. induction(eq_dec_points A C). subst C. spliter. apply l7_3 in H1. subst M. unfold Midpoint in H2. spliter. unfold Parallelogram_flat. repeat split. Col. apply bet_col in H1. Col. Cong. Cong. right. auto. spliter. eapply (mid_plgf_aux C D A B M). auto. unfold Midpoint in *. spliter. apply bet_col in H1. apply bet_col in H2. assert( M <> C). intro. subst M. apply cong_identity in H5. contradiction. assert( M <> B). intro. subst M. apply cong_symmetry in H4. apply cong_identity in H4. contradiction. ColR. Midpoint. Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel