proposition: Lemma col_cong_mid : forall A B A' B', Par A B A' B' -> ~ Par_strict 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. unfold Par in H. induction H. contradiction. spliter. induction (eq_dec_points A A'). subst A'. assert(B = B' \/ Midpoint A B B'). eapply l7_20; auto. induction H5. 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 H6. 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 H7. 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 H8. 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 H10. induction H4. assert( HH:= midpoint_existence A' B). ex_and HH M. exists M. right. assert(HH:= H11). unfold Midpoint in HH. spliter. split. assert(Bet B M B'). apply between_exchange4 with A'. Between. assumption. assert(Bet A M B'). eapply between_exchange2. apply H10. assumption. assert(Cong A M B' M). eapply (l2_11 A B _ _ A'). eapply between_inner_transitivity. apply H10. assumption. eapply between_inner_transitivity. apply between_symmetry. apply H4. assumption. Cong. Cong. unfold Midpoint. split. assumption. Cong. apply l7_2. assumption. induction H4. assert( HH:= midpoint_existence B B'). ex_and HH M. exists M. left. assert(HH:= H11). unfold Midpoint in HH. spliter. split. assert(Bet A' M B). eapply between_exchange2. apply H4. Between. assert(Bet M B A). eapply between_exchange3. apply between_symmetry. apply H12. Between. assert(Bet A' M A). eapply outer_transitivity_between. apply H14. assumption. intro. subst M. apply is_midpoint_id in H11. contradiction. assert(Cong A M A' M). eapply l2_11. apply between_symmetry. apply H15. eapply between_inner_transitivity. apply H4. Between. assumption. 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. assert(HH:=H12). unfold Midpoint in HH. spliter. split. assert(Bet B M A). eapply between_exchange4. apply between_symmetry. apply H13. assumption. assert(Bet B' B M). eapply between_inner_transitivity. apply between_symmetry. apply H10. assumption. assert(Bet M A' A). apply (between_exchange3 B). Between. assumption. assert(Bet B' M A'). eapply outer_transitivity_between2. apply H16. Between. intro. subst M. apply l7_2 in H12. apply is_midpoint_id in H12. auto. assert(Bet B' M A). eapply outer_transitivity_between. apply H18. assumption. intro. subst A'. apply is_midpoint_id in H12. subst M. tauto. assert(Cong A M B' M). eapply l4_3. apply between_symmetry. apply H15. apply H18. Cong. Cong. unfold Midpoint. split. Between. Cong. Midpoint. induction H10. induction H3. assert(B' = B /\ A = A'). eapply bet_cong_eq. assumption. Between. Cong. spliter. contradiction. induction H3. assert(Bet B' B A'). eapply bet_cong_bet. apply H7. Between. Between. Cong. assert( HH:= midpoint_existence B B'). ex_and HH M. exists M. assert(HH:=H12). unfold Midpoint in HH. spliter. left. split. assert(Bet A' M B'). eapply between_exchange2. apply between_symmetry. apply H11. assumption. assert(Bet M B' A). eapply between_exchange3. apply H13. assumption. assert(Bet A' M A). eapply outer_transitivity_between. apply H15. assumption. intro. subst M. apply l7_2 in H12. apply is_midpoint_id in H12. subst B'. tauto. assert(Bet A M B). eapply outer_transitivity_between2. apply between_symmetry. apply H16. Between. intro. subst M. apply l7_2 in H12. apply is_midpoint_id in H12. subst B'. tauto. assert(Cong A' M A M). eapply l4_3. apply H15. apply H18. Cong. Cong. unfold Midpoint. split. Between. Cong. assumption. assert( HH:= midpoint_existence A B'). ex_and HH M. exists M. assert(HH:=H11). unfold Midpoint in HH. spliter. right. split. assumption. assert(Bet A' A M). eapply between_inner_transitivity. apply between_symmetry. apply H3. assumption. assert(Bet A M B). eapply between_exchange4. apply H11. Between. assert(Bet A' M B). eapply outer_transitivity_between2. apply H14. assumption. intro. subst M. apply is_midpoint_id in H11. contradiction. assert(Cong B M A' M). eapply l4_3. apply between_symmetry. apply H15. eapply between_exchange2. apply between_symmetry. apply H3. assumption. Cong. Cong. unfold Midpoint. split. Between. Cong. induction H9. assert(Bet B' B A'). eapply outer_transitivity_between2. apply H10. assumption. assumption. assert(B = A' /\ B' = A). eapply bet_cong_eq. assumption. assumption. Cong. spliter. subst A'. tauto. induction H9. assert( HH:= midpoint_existence A A'). ex_and HH M. exists M. assert(HH:=H11). unfold Midpoint in HH. spliter. left. split. assumption. assert(Bet B A' M). eapply between_inner_transitivity. apply H9. Between. assert(Bet B M A). eapply outer_transitivity_between2. apply H14. Between. intro. subst M. apply l7_2 in H11. apply is_midpoint_id in H11. subst A'. tauto. assert(Bet B M B'). eapply between_exchange4. apply H15. Between. assert(Cong B M B' M). eapply l4_3. apply H15. assert(Bet B' A A'). eapply between_inner_transitivity. apply H10. Between. eapply between_exchange2. apply H17. assumption. Cong. Cong. unfold Midpoint. split. assumption. Cong. assert(Bet A B' A' \/ Bet A A' B'). eapply (l5_2 B). auto. Between. Between. induction H11. assert( HH:= midpoint_existence A B'). ex_and HH M. exists M. assert(HH:=H12). unfold Midpoint in HH. spliter. right. split. assumption. assert(Bet B M B'). eapply between_exchange2. apply between_symmetry. apply H10. assumption. assert(Bet A' B' M). eapply between_inner_transitivity. apply between_symmetry. apply H11. Between. assert(Bet A' M B). eapply outer_transitivity_between2. apply H16. Between. intro. subst M. apply l7_2 in H12. apply is_midpoint_id in H12. subst B'. tauto. assert(Cong M A' M B). eapply l2_11. apply between_symmetry. apply H16. eapply between_exchange3. apply between_symmetry. apply H13. assumption. Cong. Cong. unfold Midpoint. split. Between. Cong. assert( HH:= midpoint_existence A A'). ex_and HH M. exists M. assert(HH:=H12). unfold Midpoint in HH. spliter. left. split. assumption. assert(Bet B A M). eapply between_inner_transitivity. apply between_symmetry. apply H9. assumption. assert(Bet B' M A). eapply between_exchange2. apply between_symmetry. apply H11. Between. assert(Bet B' M B). eapply outer_transitivity_between. apply H16. Between. intro. subst M. apply is_midpoint_id in H12. contradiction. assert(Cong B' M B M). eapply l2_11. eapply between_inner_transitivity. apply between_symmetry. apply H11. Between. apply H15. Cong. Cong. unfold Midpoint. split. Between. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel