proposition: Lemma ts_per_per_ts : forall A B C D, TS A B C D -> Per B C A -> Per B D A -> TS C D A B.
proof: Proof. intros. assert(HTS:= H). unfold TS in H. assert (~ Col C A B). spliter. assumption. spliter. clear H. assert (A <> B). intro. subst B. Col. ex_and H4 P. assert_diffs. show_distinct C D. contradiction. unfold TS. repeat split; auto. intro. assert(A = P). apply bet_col in H5. apply (l6_21 A B C D); Col. subst P. apply H6. apply(per2_col_eq A C D B); Perp. Col. intro. assert(B = P). apply bet_col in H5. apply (l6_21 A B C D); Col. subst P. apply H6. apply(per2_col_eq B C D A); Col. exists P. split. Col. assert(exists X : Tpoint, Col A B X /\ Perp A B C X). apply(l8_18_existence A B C); Col. ex_and H7 C'. assert(exists X : Tpoint, Col A B X /\ Perp A B D X). apply(l8_18_existence A B D); Col. ex_and H12 D'. assert( A <> C'). intro. subst C'. apply perp_perp_in in H8. apply perp_in_comm in H8. apply perp_in_per in H8. assert(A = C). apply (l8_7 B); Perp. subst C. tauto. assert( A <> D'). intro. subst D'. apply perp_perp_in in H14. apply perp_in_comm in H14. apply perp_in_per in H14. assert(A = D). apply (l8_7 B); Perp. subst D. tauto. assert(Bet A C' B). apply(perp_per_bet A C B C'); Col. Perp. assert(Perp A C' C' C). apply(perp_col _ B); Col; Perp. apply perp_in_sym. apply perp_in_right_comm. apply(l8_15_1 A B C C'); auto. assert(Bet A D' B). apply(perp_per_bet A D B D'); Col. Perp. assert(Perp A D' D' D). apply(perp_col _ B); Col; Perp. apply perp_in_sym. apply perp_in_right_comm. apply(l8_15_1 A B D D'); auto. induction(eq_dec_points C' P). subst C'. assumption. induction(eq_dec_points D' P). subst D'. assumption. induction(eq_dec_points A P). subst P. Between. induction(eq_dec_points B P). subst P. Between. assert(Bet C' P D'). apply(per13_preserves_bet C P D C' D'); Col. ColR. assert(Perp P C' C' C). apply(perp_col _ A);auto. apply perp_left_comm. apply(perp_col _ B);Perp. Col. ColR. apply perp_comm in H24. apply perp_perp_in in H24. apply perp_in_comm in H24. apply perp_in_per in H24. assumption. assert(Perp P D' D' D). apply(perp_col _ A);auto. apply perp_left_comm. apply(perp_col _ B);Perp. Col. ColR. apply perp_comm in H24. apply perp_perp_in in H24. apply perp_in_comm in H24. apply perp_in_per in H24. assumption. apply bet3__bet with C' D'; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel