proposition: Lemma l9_8_2 : forall P Q A B C, TS P Q A C -> OS P Q A B -> TS P Q B C.
proof: Proof. intros. unfold OS in H0. ex_and H0 D. assert (HH:= H). assert (HH0:=H0). assert (HH1:=H1). unfold TS in HH1. assert (P <> Q). intro. subst Q. spliter. Col. spliter. unfold TS in HH0. assert (P <> Q). intro. subst Q. spliter. Col. spliter. unfold TS in HH. assert (P <> Q). intro. subst Q. spliter. Col. spliter. ex_and H13 T. ex_and H9 X. ex_and H5 Y. assert (exists M , Bet Y M A /\ Bet X M B). eapply inner_pasch. apply H16. apply H15. ex_and H17 M. assert (A <> D). intro. subst D. apply not_two_sides_id in H0. assumption. assert (B <> D). intro. subst D. apply not_two_sides_id in H1. assumption. induction (col_dec A B D). induction (eq_dec_points M Y). subst M. assert (X = Y). apply l6_21 with P Q A D; Col; ColR. subst Y. eapply l9_5. apply H. apply H9. unfold Out. repeat split. intro. subst X. apply H11. assumption. intro. subst X. apply H3. assumption. unfold Col in H21. induction H21. right. eapply between_exchange3. apply between_symmetry. apply H16. apply between_symmetry. assumption. induction H21. assert (Bet D B A \/ Bet D A B). eapply (l5_1 _ X). intro. subst X. apply H4. assumption. apply between_symmetry. assumption. apply between_symmetry. assumption. induction H22. assert (D = B). eapply between_equality. apply H22. apply H21. subst D. absurde. assert (D = A). eapply between_equality. apply H22. apply between_symmetry. assumption. subst D. absurde. eapply (l5_2 D). intro. subst X. apply H8. assumption. apply between_symmetry. assumption. apply between_symmetry. assumption. induction (eq_dec_points M X). subst M. assert (X = Y). apply l6_21 with P Q A D; Col; ColR. subst Y. absurde. eapply (l9_5 _ _ M _ X). eapply l9_5. apply H. apply H5. unfold Out. repeat split. intro. subst Y. apply between_identity in H17. subst M. absurde. assumption. right. assumption. assumption. unfold Out. assert (Out Y M A). unfold Out. repeat split. assumption. intro. subst Y. apply H11. assumption. left. assumption. repeat split. assumption. intro. subst X. apply between_identity in H18. subst M. absurde. left. apply H18. eapply (l9_5 _ _ M). eapply l9_5. apply H. apply H5. unfold Out. repeat split. intro. subst Y. apply H7. assumption. intro. subst Y. assert(Col B D X). eapply (col_transitivity_1 _ M). intro. subst M. apply H3. assumption. unfold Col. left. assumption. unfold Col. left. apply between_symmetry. assumption. apply H21. apply col_permutation_1. eapply (col_transitivity_1 _ X). intro. subst X. apply H4. assumption. unfold Col. left. apply between_symmetry. assumption. apply col_permutation_1. assumption. right. assumption. apply H9. unfold Out. repeat split. intro. subst X. assert (Col A D Y). eapply (col_transitivity_1 _ M). intro. subst M. apply H7. assumption. unfold Col. left. assumption. unfold Col. left. apply between_symmetry. assumption. apply H21. apply col_permutation_1. eapply (col_transitivity_1 _ Y). intro. subst Y. apply H4. assumption. apply col_permutation_1. assumption. unfold Col. left. apply between_symmetry. assumption. intro. subst X. apply H3. assumption. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar