proposition: Lemma par_two_sides_two_sides : forall A B C D, Par A B C D -> TS B D A C -> TS A C B D.
proof: Proof. intros. apply par_distincts in H. spliter. unfold Par in H. induction H. assert_diffs. unfold TS in *. spliter. ex_and H6 T. repeat split. intro. assert(Col T B C). apply col_permutation_1. apply (col_transitivity_1 _ A); Col. apply H3. apply col_permutation_2. eapply (col_transitivity_1 _ T). intro. treat_equalities. apply par_strict_not_col_1 in H. Col. Col. Col. intro. assert(Col T C D). apply col_permutation_2. apply (col_transitivity_1 _ A); Col. apply H3. apply col_permutation_1. apply (col_transitivity_1 _ T). intro. treat_equalities. apply par_strict_not_col_3 in H. Col. Col. Col. exists T. split. apply bet_col in H8. Col. induction H6. assert(HH:= outer_pasch C D T A B (between_symmetry _ _ _ H8) (between_symmetry _ _ _ H6)). ex_and HH X. unfold Par_strict in H. spliter. apply False_ind. apply H12. exists X. split; Col. induction H6. assert(HH:= outer_pasch A B T C D H8 H6). ex_and HH X. apply False_ind. unfold Par_strict in H. spliter. apply H12. exists X. split; Col. apply between_symmetry. assumption. unfold TS in H0. spliter. apply False_ind. apply H3. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles