proposition: Lemma plgf_mid : forall A B C D, Parallelogram_flat A B C D -> exists M, Midpoint M A C /\ Midpoint M B D.
proof: Proof. intros. unfold Parallelogram_flat in H. spliter. induction(eq_dec_points A B). subst B. apply cong_symmetry in H1. apply cong_identity in H1. subst D. assert(HH:=midpoint_existence A C). ex_and HH M. exists M. split; assumption. assert(C <> D). intro. subst D. apply cong_identity in H1. contradiction. assert(Par A B C D). apply par_symmetry. unfold Par. right. repeat split; Col. assert(~Par_strict A B C D). intro. unfold Par_strict in H7. spliter. apply H8. exists C. split; Col. assert(HH:= col_cong_mid A B C D H6 H7 H1). ex_and HH M. induction H8. exists M. assumption. spliter. induction(eq_dec_points B C). subst C. apply cong_identity in H2. subst D. apply l7_3 in H8. apply l7_3 in H9. subst M. contradiction. assert(A <> D). intro. subst D. apply cong_symmetry in H2. apply cong_identity in H2. subst C. tauto. apply False_ind. assert(Col A B M). unfold Midpoint in *. spliter. eapply (col_transitivity_1 _ D). assumption. Col. apply bet_col in H8. Col. assert(B <> M). intro. subst M. apply is_midpoint_id in H9. contradiction. assert(A <> M). intro. subst M. apply is_midpoint_id in H8. contradiction. induction H12. assert(HH:=symmetry_preserves_bet B A M C D H9 H8). destruct HH. assert(Bet M C D). apply H16. Between. clear H15 H16. assert(B = A /\ D = C). unfold Midpoint in *. spliter. apply bet_cong_eq. eBetween. eBetween. Cong. spliter. subst B. tauto. induction H12. assert(Bet M A C \/ Bet M C A). unfold Midpoint in *. spliter. eapply (l5_2 B); assumption. induction H15. assert(Bet M D B <-> Bet M A C). apply(symmetry_preserves_bet A C M D B). assumption. Midpoint. destruct H16. assert(Bet M D B). apply H17. assumption. clear H17 H16. assert(A = C /\ B = D). unfold Midpoint in *. spliter. apply bet_cong_eq. eBetween. eBetween. Cong. spliter. subst C. induction H3. tauto. subst D. tauto. assert(Bet M B D <-> Bet M C A). apply(symmetry_preserves_bet); Midpoint. destruct H16. assert(Bet M B D). apply H17. assumption. clear H16 H17. assert(C = A /\ D = B). unfold Midpoint in *. spliter. apply bet_cong_eq. eBetween. eBetween. Cong. spliter. subst C. induction H3. tauto. subst D. tauto. assert(HH:=symmetry_preserves_bet A B M D C H8 H9). destruct HH. assert(Bet M D C). apply H16. Between. clear H15 H16. assert(A = B /\ C = D). unfold Midpoint in *. spliter. apply bet_cong_eq. eBetween. eBetween. Cong. spliter. subst B. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel