proposition: Lemma mid_plgf_aux : forall A B C D M, A <> C -> Col A B C -> Midpoint M A C -> Midpoint M B D -> Parallelogram_flat A B C D.
proof: Proof. intros. unfold Parallelogram_flat. induction(eq_dec_points B D). subst D. apply l7_3 in H2. subst M. unfold Midpoint in H1. spliter. repeat split; Col. Cong. Cong. assert(Col A B M). unfold Midpoint in *. spliter. apply bet_col in H1. apply bet_col in H2. ColR. assert(M <> B). intro. subst M. apply is_midpoint_id in H2. contradiction. assert(M <> A). intro. subst M. apply is_midpoint_id in H1. contradiction. induction H4. assert(HH:=symmetry_preserves_bet B A M D C H2 H1). destruct HH. assert(Bet M D C). apply H8. Between. clear H8 H7. repeat split. Col. unfold Midpoint in *. spliter. apply bet_col in H2. apply bet_col in H1. apply bet_col in H4. ColR. eapply l4_3. apply H4. apply between_symmetry. apply H9. unfold Midpoint in H1. spliter. Cong. unfold Midpoint in H2. spliter. Cong. unfold Midpoint in *. spliter. eapply (l2_11 _ M _ _ M _). eBetween. eBetween. Cong. Cong. left. assumption. induction H4. assert(Bet M A D \/ Bet M D A). eapply (l5_2 B). auto. assumption. unfold Midpoint in H2. spliter. assumption. induction H7. assert(Bet M C B <-> Bet M A D). apply (symmetry_preserves_bet A D M C B). assumption. Midpoint. destruct H8. assert(Bet M C B). apply H9. assumption. clear H9 H8. unfold Midpoint in *. spliter. repeat split. assumption. apply bet_col in H4. apply bet_col in H1. apply bet_col in H2. ColR. eapply (l2_11 _ M _ _ M _). Between. eBetween. Cong. Cong. apply cong_commutativity. eapply (l4_3). apply between_symmetry. apply H7. apply between_symmetry. apply H10. Cong. Cong. left. assumption. assert(Bet M B C <-> Bet M D A). apply (symmetry_preserves_bet D A M B C). Midpoint. Midpoint. destruct H8. assert(Bet M B C). apply H9. assumption. clear H8 H9. unfold Midpoint in *. spliter. repeat split. assumption. apply bet_col in H4. apply bet_col in H1. apply bet_col in H2. ColR. eapply (l2_11 _ M _ _ M _). Between. eBetween. Cong. Cong. eapply l4_3. apply between_symmetry. apply H7. apply between_symmetry. apply H10. Cong. Cong. left. assumption. assert(Bet M C D <-> Bet M A B). apply (symmetry_preserves_bet A B M C D H1 H2). destruct H7. assert(Bet M C D). apply H8. assumption. clear H8 H7. repeat split. Col. unfold Midpoint in *. spliter. apply bet_col in H2. apply bet_col in H1. apply bet_col in H4. ColR. apply cong_commutativity. eapply l4_3. apply between_symmetry. apply H4. apply between_symmetry. apply H9. unfold Midpoint in H2. spliter. Cong. unfold Midpoint in H1. spliter. Cong. unfold Midpoint in *. spliter. eapply (l2_11 _ M _ _ M _). eBetween. eBetween. Cong. Cong. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel