proposition: Lemma par_cong_mid : forall A B A' B', Par A B A' B' -> Cong A B A' B' -> exists M, Midpoint M A A' /\ Midpoint M B B' \/ Midpoint M A B' /\ Midpoint M B A'.
proof: Proof. intros. induction H. assert(HH:= cop__one_or_two_sides A A' B B'). assert(HH0:= H). unfold Par_strict in HH0. spliter. assert(TS A A' B B' \/ OS A A' B B'). apply HH. Cop. intro. apply H2. exists A'. split;Col. intro. apply H2. exists A. split; Col. induction H3. clear HH. assert(HH:= H3). unfold TS in HH. assert(~ Col B A A'). spliter. assumption. spliter. ex_and H7 M. exists M. left. assert(B <> B'). intro. subst B'. apply between_identity in H8. subst M. apply H2. exists B. split; Col. induction (eq_dec_points B M). subst M. contradiction. induction (eq_dec_points B' M). subst M. apply False_ind. apply H6. Col. assert(A <> A'). intro. subst A'. apply False_ind. apply H6. Col. assert(A <> M). intro. subst M. apply H2. exists B'. split. apply bet_col in H8. Col. Col. assert(A' <> M). intro. subst M. apply H2. exists B. apply bet_col in H8. split. Col. Col. assert(HH:=(midpoint_existence A A')). ex_and HH X. prolong B X B'' B X. assert(Midpoint X B B''). unfold Midpoint. split. assumption. Cong. assert(Par_strict B A B'' A'). apply (midpoint_par_strict B A B'' A' X); auto. assert(Col B'' B' A' /\ Col A' B' A'). apply(parallel_uniqueness B A B' A' B'' A' A'). apply par_comm. unfold Par. left. assumption. Col. unfold Par. left. assumption. Col. spliter. assert(Cong A B A' B''). eapply l7_13. apply l7_2. apply H15. apply l7_2. assumption. assert(Cong A' B' A' B''). eapply cong_transitivity. apply cong_symmetry. apply H0. assumption. assert(B' = B'' \/ Midpoint A' B' B''). eapply l7_20. Col. Cong. induction H24. subst B''. assert(X = M). eapply (l6_21 A A' B B'); Col. subst X. split; auto. assert(TS A A' B B''). unfold TS. repeat split; auto. intro. apply H6. apply col_permutation_1. eapply (col_transitivity_1 _ B''). intro. subst B''. apply l7_2 in H24. apply is_midpoint_id in H24. apply par_strict_distinct in H; spliter; auto. Col. Col. exists X. split. unfold Midpoint in H15. spliter. apply bet_col in H15. Col. assumption. assert(OS A A' B' B''). eapply l9_8_1. apply l9_2. apply H3. apply l9_2. assumption. assert(TS A A' B' B''). unfold TS. repeat split. intro. apply H6. Col. intro. apply H6. apply col_permutation_1. eapply (col_transitivity_1 _ B''). intro. subst B''. apply l7_2 in H24. apply is_midpoint_id in H24. apply par_strict_distinct in H; spliter; auto. Col. Col. exists A'. split. Col. unfold Midpoint in H24. spliter. assumption. apply l9_9 in H27. contradiction. clear HH H1. assert(HH:=(midpoint_existence A' B)). ex_and HH X. exists X. right. prolong A X B'' A X. assert(Midpoint X A B''). unfold Midpoint. split. assumption. Cong. assert(~Col A B A'). intro. apply H2. exists A'. split; Col. assert(Par_strict A B B'' A'). apply (midpoint_par_strict A B B'' A' X). assumption. assumption. apply l7_2. assumption. assert(Col B'' B' A' /\ Col A' B' A'). apply (parallel_uniqueness B A B' A' B'' A' A'). apply par_comm. unfold Par. left. assumption. Col. apply par_left_comm. unfold Par. left. assumption. Col. spliter. assert(Cong A B B'' A'). eapply l7_13. apply l7_2. apply H6. assumption. assert(Cong A' B' A' B''). eapply cong_transitivity. apply cong_symmetry. apply H0. Cong. assert(B' = B'' \/ Midpoint A' B' B''). eapply l7_20. Col. Cong. induction H13. subst B''. split. assumption. apply l7_2. assumption. assert(OS A A' X B''). eapply (out_one_side_1 _ _ X B''). intro. apply H7. apply col_permutation_1. eapply (col_transitivity_1 _ X). intro. subst X. apply is_midpoint_id in H1. subst A'. apply H2. exists B. split; Col. Col. unfold Midpoint in H1. spliter. apply bet_col in H1. Col. Col. unfold Out. repeat split. intro. subst X. apply cong_identity in H5. subst B''. unfold Par_strict in H8. spliter. apply H8. exists A. split; Col. intro. subst B''. unfold Par_strict in H8. spliter. apply H14. exists A. split; Col. unfold Midpoint in H6. spliter. left. assumption. assert(TS A A' B' B''). unfold TS. repeat split. intro. apply H2. exists A. split; Col. unfold OS in H14. ex_and H14 T. unfold TS in H15. spliter. assumption. exists A'. split. Col. unfold Midpoint in H13. spliter. assumption. assert(TS A A' X B'). eapply l9_8_2. apply l9_2. apply H15. apply one_side_symmetry. assumption. assert(OS A A' X B). eapply (out_one_side_1). intro. apply H7. apply col_permutation_1. eapply (col_transitivity_1 _ X). intro. subst X. apply is_midpoint_id in H1. subst A'. apply H2. exists B. split; Col. Col. unfold Midpoint in H1. spliter. apply bet_col in H1. Col. apply col_trivial_2;assumption. unfold Out. repeat split. intro. subst X. unfold TS in H16. spliter. apply H16. Col. intro. subst A'. unfold Par_strict in H8. spliter. apply H17. exists B. split; Col. unfold Midpoint in H1. spliter. left. assumption. assert(OS A A' X B'). eapply one_side_transitivity. apply H17. assumption. apply l9_9 in H16. contradiction. spliter. induction (eq_dec_points A A'). subst A'. assert(B = B' \/ Midpoint A B B'). eapply l7_20; auto. induction H4. subst B'. assert( HH:= midpoint_existence A B). ex_and HH M. exists M. right. split. assumption. apply l7_2. assumption. exists A. left. split. apply l7_3_2. assumption. induction (eq_dec_points B B'). subst B'. assert(A = A' \/ Midpoint B A A'). eapply l7_20. Col. Cong. induction H5. subst A'. assert( HH:= midpoint_existence A B). ex_and HH M. exists M. right. split. assumption. apply l7_2. assumption. exists B. left. split. assumption. apply l7_3_2. induction (eq_dec_points A B'). subst B'. assert(B = A' \/ Midpoint A B A'). eapply l7_20. Col. Cong. induction H6. subst A'. assert( HH:= midpoint_existence A B). ex_and HH M. exists M. left. split. assumption. apply l7_2. assumption. exists A. right. split. apply l7_3_2. assumption. induction (eq_dec_points A' B). subst A'. assert(A = B' \/ Midpoint B A B'). eapply l7_20. Col. Cong. induction H7. subst B'. assert( HH:= midpoint_existence A B). ex_and HH M. exists M. left. split. assumption. apply l7_2. assumption. exists B. right. split. assumption. apply l7_3_2. assert(Col A B A'). ColR. assert(Col A B B'). ColR. induction H9. induction H3. assert( HH:= midpoint_existence A' B). ex_and HH M. exists M. right. split. assert(Bet B M B'). apply between_exchange4 with A'. Between. assumption. assert(Bet A M B'). eapply between_exchange2. apply H9. assumption. assert(Cong A M B' M). eapply (l2_11 A B _ _ A'). eapply between_inner_transitivity. apply H9. assumption. eapply between_inner_transitivity. apply between_symmetry. apply H3. unfold Midpoint in H10. spliter. assumption. Cong. unfold Midpoint in H10. spliter. apply cong_left_commutativity. Cong. unfold Midpoint. split. assumption. Cong. apply l7_2. assumption. induction H3. assert( HH:= midpoint_existence B B'). ex_and HH M. exists M. left. split. assert(Bet A' M B). eapply between_exchange2. apply H3. unfold Midpoint in H10. spliter. Between. assert(Bet M B A). eapply between_exchange3. unfold Midpoint in H10. spliter. apply between_symmetry. apply H10. Between. assert(Bet A' M A). eapply outer_transitivity_between. apply H11. assumption. intro. subst M. apply is_midpoint_id in H10. contradiction. assert(Cong A M A' M). eapply l2_11. apply between_symmetry. apply H12. eapply between_inner_transitivity. apply H3. unfold Midpoint in H10. spliter. Between. assumption. unfold Midpoint in H10. spliter. Cong. unfold Midpoint. split. Between. Cong. assumption. assert(Bet B A' A). eapply (bet_cong_bet B'). auto. Between. Between. Cong. assert( HH:= midpoint_existence A' B). ex_and HH M. exists M. right. split. assert(Bet B M A). eapply between_exchange4. unfold Midpoint in H11. spliter. apply between_symmetry. apply H11. assumption. assert(Bet B' B M). eapply between_inner_transitivity. apply between_symmetry. apply H9. assumption. assert(Bet M A' A). apply (between_exchange3 B). Between. assumption. assert(Bet B' M A'). eapply outer_transitivity_between2. apply H13. unfold Midpoint in H11. spliter. Between. intro. subst M. apply l7_2 in H11. apply is_midpoint_id in H11. auto. assert(Bet B' M A). eapply outer_transitivity_between. apply H15. assumption. intro. subst A'. apply is_midpoint_id in H11. subst M. tauto. assert(Cong A M B' M). eapply l4_3. apply between_symmetry. apply H12. apply H15. Cong. unfold Midpoint in H11. spliter. Cong. unfold Midpoint. split. Between. Cong. Midpoint. induction H9. induction H2. assert(B' = B /\ A = A'). eapply bet_cong_eq. assumption. Between. Cong. spliter. contradiction. induction H2. assert(Bet B' B A'). eapply bet_cong_bet. apply H6. Between. Between. Cong. assert( HH:= midpoint_existence B B'). ex_and HH M. exists M. left. split. assert(Bet A' M B'). eapply between_exchange2. apply between_symmetry. apply H10. unfold Midpoint in H11. spliter. assumption. assert(Bet M B' A). eapply between_exchange3. unfold Midpoint in H11. spliter. apply H11. assumption. assert(Bet A' M A). eapply outer_transitivity_between. apply H12. assumption. intro. subst M. apply l7_2 in H11. apply is_midpoint_id in H11. apply sym_equal in H11. contradiction. assert(Bet A M B). eapply outer_transitivity_between2. apply between_symmetry. apply H13. unfold Midpoint in H11. spliter. Between. intro. subst M. apply l7_2 in H11. apply is_midpoint_id in H11. apply sym_equal in H11. contradiction. assert(Cong A' M A M). eapply l4_3. apply H12. apply H15. Cong. unfold Midpoint in H11. spliter. Cong. unfold Midpoint. split. Between. Cong. assumption. assert( HH:= midpoint_existence A B'). ex_and HH M. exists M. right. split. assumption. assert(Bet A' A M). eapply between_inner_transitivity. apply between_symmetry. apply H2. unfold Midpoint in H10. spliter. assumption. assert(Bet A M B). eapply between_exchange4. unfold Midpoint in H10. spliter. apply H10. Between. assert(Bet A' M B). eapply outer_transitivity_between2. apply H11. assumption. intro. subst M. apply is_midpoint_id in H10. contradiction. assert(Cong B M A' M). eapply l4_3. apply between_symmetry. apply H12. eapply between_exchange2. apply between_symmetry. apply H2. unfold Midpoint in H10. spliter. assumption. Cong. unfold Midpoint in H10. spliter. Cong. unfold Midpoint. split. Between. Cong. induction H8. assert(Bet B' B A'). eapply outer_transitivity_between2. apply H9. assumption. assumption. assert(B = A' /\ B' = A). eapply bet_cong_eq. assumption. assumption. Cong. spliter. subst A'. tauto. induction H8. assert( HH:= midpoint_existence A A'). ex_and HH M. exists M. left. split. assumption. assert(Bet B A' M). eapply between_inner_transitivity. apply H8. unfold Midpoint in H10. spliter. Between. assert(Bet B M A). eapply outer_transitivity_between2. apply H11. unfold Midpoint in H10. spliter. Between. intro. subst M. apply l7_2 in H10. apply is_midpoint_id in H10. subst A'. tauto. assert(Bet B M B'). eapply between_exchange4. apply H12. Between. assert(Cong B M B' M). eapply l4_3. apply H12. assert(Bet B' A A'). eapply between_inner_transitivity. apply H9. Between. eapply between_exchange2. apply H14. unfold Midpoint in H10. spliter. Between. Cong. unfold Midpoint in H10. spliter. Cong. unfold Midpoint. split. assumption. Cong. assert(Bet A B' A' \/ Bet A A' B'). eapply (l5_2 B). auto. Between. Between. induction H10. assert( HH:= midpoint_existence A B'). ex_and HH M. exists M. right. split. assumption. assert(Bet B M B'). eapply between_exchange2. apply between_symmetry. apply H9. unfold Midpoint in H11. spliter. Between. assert(Bet A' B' M). eapply between_inner_transitivity. apply between_symmetry. apply H10. unfold Midpoint in H11. spliter. Between. assert(Bet A' M B). eapply outer_transitivity_between2. apply H13. Between. intro. subst M. apply l7_2 in H11. apply is_midpoint_id in H11. subst B'. tauto. assert(Cong M A' M B). eapply l2_11. apply between_symmetry. apply H13. eapply between_exchange3. unfold Midpoint in H11. spliter. apply between_symmetry. apply H11. assumption. unfold Midpoint in H11. spliter. Between. Cong. Cong. unfold Midpoint. split. Between. Cong. assert( HH:= midpoint_existence A A'). ex_and HH M. exists M. left. split. assumption. assert(Bet B A M). eapply between_inner_transitivity. apply between_symmetry. apply H8. unfold Midpoint in H11. spliter. Between. assert(Bet B' M A). eapply between_exchange2. apply between_symmetry. apply H10. unfold Midpoint in H11. spliter. Between. assert(Bet B' M B). eapply outer_transitivity_between. apply H13. Between. intro. subst M. apply is_midpoint_id in H11. contradiction. assert(Cong B' M B M). eapply l2_11. eapply between_inner_transitivity. apply between_symmetry. apply H10. unfold Midpoint in H11. spliter. Between. apply H12. Cong. unfold Midpoint in H11. spliter. Between. Cong. unfold Midpoint. split. Between. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec