proposition: Lemma l8_21_aux : forall A B C, ~ Col A B C -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
proof: Proof. intros. assert (exists X : Tpoint, Col A B X /\ Perp A B C X). eapply l8_18_existence. assumption. ex_and H0 X. assert (Perp_at X A B C X). eapply l8_15_1; assert_diffs; auto. assert (Per A X C). unfold Perp_at in H2. spliter. apply H6. apply col_trivial_1. apply col_trivial_1. assert(HH:= H3). unfold Per in H3. ex_and H3 C'. double C A C''. assert (exists P, Midpoint P C' C''). eapply l7_25. unfold Midpoint in *. spliter. eapply cong_transitivity. apply cong_symmetry. apply H4. apply cong_left_commutativity. assumption; spliter. ex_elim H6 P. assert (Per X A P). eapply l8_20_1. apply HH. apply l7_2. apply H7. apply l7_2. apply H5. apply l7_2. assumption. assert (X <> C). intro. subst C. apply H. assumption. assert (A <> P). eapply l8_20_2. apply HH. apply l7_2. apply H7. apply l7_2. assumption. apply l7_2. assumption. assumption. assert (exists T, Bet P T C /\ Bet A T X). eapply l3_17. apply midpoint_bet. apply l7_2. apply H5. apply midpoint_bet. apply l7_2. apply H3. apply midpoint_bet. apply l7_2. apply H7. ex_and H10 T. induction (eq_dec_points A X). subst X. exists P. exists T. apply between_identity in H11. subst T. assert (C'= C''). eapply symmetric_point_uniqueness. apply H3. assumption. subst C''. apply l7_3 in H7. subst P. assert (Col A C C') by ColR. repeat split;Col;Between. apply perp_col0 with C A;auto using perp_sym;Col. exists P. exists T. repeat split. unfold Perp. exists A. unfold Perp_at. repeat split. assert_diffs; auto. auto. apply col_trivial_1. apply col_trivial_3. unfold Perp_at in H2. spliter. intros. eapply per_col in H6. apply l8_2 in H6. eapply per_col in H6. eapply l8_2 in H6. apply H6. assumption. ColR. assumption. ColR. ColR. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR