proposition: Lemma l9_5 : forall P Q A C R B, TS P Q A C -> Col R P Q -> Out R A B -> TS P Q B C.
proof: Proof. intros. assert (P <> Q). unfold TS in H. spliter. intro. subst Q. Col. assert(exists A0, Col P Q A0 /\ Perp P Q A A0). eapply l8_18_existence. intro. unfold TS in H. spliter. apply H. apply col_permutation_2. assumption. assert(exists C0, Col P Q C0 /\ Perp P Q C C0). eapply l8_18_existence. unfold TS in H. spliter. intro. apply H4. apply col_permutation_2. assumption. assert(exists B0, Col P Q B0 /\ Perp P Q B B0). eapply l8_18_existence. assert (HH1:=H1). unfold Out in HH1. unfold TS in H. spliter. intro. assert (Col P B R). eapply col_transitivity_1. apply H2. assumption. apply col_permutation_1. assumption. assert (R <> B). intro. subst B. absurde. assert(Col R P A ). eapply col_transitivity_1. apply H12. eapply col_permutation_3. assumption. apply col_permutation_5. apply out_col. assumption. apply H. ColR. ex_and H3 A'. ex_and H4 C'. ex_and H5 B'. assert (exists M, Midpoint M A' C'). apply midpoint_existence. ex_and H9 M. double A M D. assert (Out C' D C <-> Out A' A A). eapply l9_4_1. apply l9_2. apply H. apply col_permutation_2. assumption. assumption. apply col_permutation_2. assumption. assumption. apply l7_2. apply H10. apply l7_2. assumption. destruct H11. assert (Out C' D C). apply H12. unfold Out. repeat split. intro. subst A'. apply perp_distinct in H6. spliter. absurde. intro. subst A'. apply perp_distinct in H6. spliter. absurde. left. apply between_trivial. assert (TS P Q A D). eapply l9_4_2. apply H. apply col_permutation_2. apply H3. assumption. apply col_permutation_2. apply H4. apply H7. unfold Out. repeat split. intro. subst A'. apply perp_distinct in H6. spliter. absurde. intro. subst A'. apply perp_distinct in H6. spliter. absurde. left. apply between_trivial. assumption. assert (TS P Q B D). apply l9_3 with A M R; trivial. induction (eq_dec_points A' C'). subst C'. apply l7_3 in H10. subst A'. apply col_permutation_2. assumption. ColR. apply l9_4_2 with B D B' C'; Col. apply perp_sym. apply perp_left_comm. eapply perp_col. intro. subst D. unfold Out in H13. spliter. absurde. apply perp_sym. apply perp_right_comm. apply H7. apply col_permutation_5. apply out_col. assumption. apply out_trivial. intro. subst B. apply perp_distinct in H8. spliter. absurde. apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar