proposition: Lemma midpoint_existence_aux : forall A B P Q T, A<>B -> Perp A B Q B -> Perp A B P A -> Col A B T -> Bet Q T P -> Le A P B Q -> exists X : Tpoint, Midpoint X A B.
proof: Proof. intros. unfold Le in H4. ex_and H4 R. assert (exists X, Bet T X B /\ Bet R X P). eapply inner_pasch. apply between_symmetry. apply H3. auto. ex_and H6 X. assert (Col A B X). induction (eq_dec_points T B). subst T. apply between_identity in H6. subst X. Col. ColR. induction(col_dec A B P). assert (B=A \/ P=A). eapply l8_9. apply perp_per_1. assumption. apply col_permutation_4. assumption. induction H10. exists A. subst B. eapply l7_3_2. treat_equalities. apply perp_distinct in H1. spliter. absurde. assert (B <> R). intro. subst R. treat_equalities. apply H9. apply col_trivial_3. assert (~Col A B Q). intro. assert (A=B \/ Q=B). eapply l8_9. apply perp_per_2. auto. apply perp_comm. assumption. assumption. induction H12. apply H. assumption. subst Q. treat_equalities. absurde. assert (~Col A B R). intro. assert (Col B A Q). ColR. Col. show_distinct P R. intuition. induction (eq_dec_points A P). subst P. apply perp_distinct in H1. 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 perp_sym. apply H0. Col. Col. apply between_symmetry in H7. assert (Cong A R P B). apply (perp_cong A B P R X); assumption. assert (Midpoint X A B /\ Midpoint X P R). apply (l7_21 A P B R X); Col; Cong. spliter. exists X. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR