proposition: Lemma l8_24 : forall A B P Q R T, Perp P A A B -> Perp Q B A B -> Col A B T -> Bet P T Q -> Bet B R Q -> Cong A P B R -> exists X, Midpoint X A B /\ Midpoint X P R.
proof: Proof. intros. unfold Le in H4. assert (exists X, Bet T X B /\ Bet R X P). eapply inner_pasch. apply H2. assumption. ex_and H5 X. assert (Col A B X). induction (eq_dec_points T B). subst T. apply between_identity in H5. subst X. apply col_trivial_2. assert (Col T X B). unfold Col. left. assumption. apply col_permutation_4. eapply col_transitivity_1. intro. apply H7. apply sym_equal. apply H9. apply col_permutation_1. assumption. apply col_permutation_2. assumption. assert (A <> B). apply perp_distinct in H. spliter. assumption. assert (A <> P). apply perp_distinct in H. spliter. auto. induction(col_dec A B P). assert (B=A \/ P=A). eapply l8_9. apply perp_per_1. apply perp_sym. assumption. apply col_permutation_4. assumption. induction H11. exists A. subst B. absurde. subst P. absurde. assert (B <> R). intro. subst R. apply cong_identity in H4. subst P. absurde. assert (Q <> B). apply perp_distinct in H0. spliter. assumption. assert (~Col A B Q). intro. assert (A=B \/ Q=B). eapply l8_9. apply perp_per_2. auto. apply perp_comm. apply perp_sym. assumption. assumption. induction H14. contradiction. subst Q. absurde. assert (~Col A B R). intro. assert (Col B A Q). eapply col_transitivity_1. apply H11. apply col_permutation_1. assumption. unfold Col. left. assumption. apply H13. apply col_permutation_4. assumption. assert (P <> R). intro. subst R. apply between_identity in H6. subst X. contradiction. induction (eq_dec_points A P). subst P. apply perp_distinct in H. spliter. absurde. assert (Perp A B R B). eapply perp_col. assumption. apply perp_sym. apply perp_left_comm. eapply perp_col. assumption. apply perp_left_comm. apply H0. unfold Col. right; left. apply between_symmetry. assumption. apply col_trivial_2. assert (Cong A R P B). apply (perp_cong A B P R X). assumption. assumption. apply perp_sym. assumption. assumption. assumption. assumption. apply between_symmetry. assumption. intros. assert (Midpoint X A B /\ Midpoint X P R). apply (l7_21 A P B R X). intro. apply H10. apply col_permutation_5. assumption. assumption. assumption. apply cong_right_commutativity. apply cong_symmetry. assumption. apply col_permutation_5. assumption. unfold Col. left. apply between_symmetry. assumption. exists X. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR