proposition: Lemma l10_15 : forall A B C P, Col A B C -> ~ Col A B P -> exists Q, Perp A B Q C /\ OS A B P Q.
proof: Proof. intros. assert (A<>B). intro;subst. Col. assert (exists X , TS A B P X). apply l9_10. intro. apply H0. apply col_permutation_1. assumption. ex_elim H2 X. induction (eq_dec_points A C). subst C. assert (exists Q, exists T, Perp A B Q A /\ Col A B T /\ Bet X T Q). apply l8_21. assumption. ex_elim H2 Q. ex_and H4 T. exists Q. split. assumption. eapply l9_8_1. apply H3. unfold TS. repeat split. apply perp_not_col in H2. intro. apply H2. apply col_permutation_1. assumption. unfold TS in H3. spliter. assumption. exists T. split. apply col_permutation_2. assumption. apply between_symmetry. assumption. assert (exists Q, exists T, Perp C A Q C /\ Col C A T /\ Bet X T Q). apply l8_21. auto. ex_elim H4 Q. ex_and H5 T. exists Q. split. eapply perp_col. assumption. apply perp_left_comm. apply H4. apply col_permutation_5. assumption. eapply l9_8_1. apply H3. unfold TS. repeat split. eapply perp_not_col in H4. intro. apply H4. apply col_permutation_2. eapply col_transitivity_1. apply H1. apply col_permutation_1. assumption. assumption. unfold TS in H3. spliter. assumption. exists T. split. apply col_permutation_2. eapply col_transitivity_1. apply H2. apply col_permutation_5. assumption. apply col_permutation_4. assumption. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop