proposition: Lemma l13_2_1 : forall A B C D E, TS A B C D -> Per B C A -> Per B D A -> Col C D E -> Perp A E C D -> CongA C A B D A B -> CongA B A C D A E /\ CongA B A D C A E /\ Bet C E D.
proof: Proof. intros. intros. assert(HH:= H). unfold TS in HH. assert (~ Col C A B). spliter. assumption. spliter. assert(A <> C /\ A <> B /\ A <> D). unfold CongA in H4. spliter. repeat split; auto. spliter. assert(Cong B C B D /\ Cong A C A D /\ CongA C B A D B A). apply(l11_50_2 B A C B A D). intro. apply H6. Col. eapply l11_16; auto. apply l8_2. auto. intro. subst C. apply H6. Col. apply l8_2. auto. intro. subst D. apply H7. Col. apply conga_comm. auto. Cong. spliter. assert(Perp C D A B). apply( cong_conga_perp C A D B); Cong. assert(Col A B E). apply cop_perp2__col with C D. exists E. left. split; Col. apply perp_sym. apply H15. auto. assert(TS C D A B). apply ts_per_per_ts; auto. unfold TS in H17. spliter. ex_and H19 T1. ex_and H8 T. assert(T = T1). apply bet_col in H20. apply bet_col in H21. assert_diffs. apply (l6_21 A B C D); Col. subst T1. assert(T = E). assert_diffs. apply (l6_21 A B C D); Col. subst T. split. apply conga_left_comm. apply l11_10 with C B D B; try apply out_trivial; auto. repeat split; auto. intro. subst E. contradiction. split. apply conga_sym. apply conga_right_comm. apply l11_10 with C B D B; try apply out_trivial; auto. repeat split; auto. intro. subst E. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel