proposition: Lemma col_two_sides_bet : forall A B X Y, Col A X Y -> TS A B X Y -> Bet X A Y.
proof: Proof. intros. unfold Col in H. induction H. unfold TS in H0. spliter. ex_and H2 T. apply False_ind. apply H1. apply col_permutation_2. eapply (col_transitivity_1 _ T). intro. subst T. assert(A = X). eapply between_equality. apply H. assumption. subst X. apply H0. apply col_trivial_1. apply col_permutation_4. assumption. apply col_permutation_1. eapply (col_transitivity_1 _ X). intro. subst Y. apply between_identity in H3. subst X. contradiction. apply bet_col in H. apply col_permutation_3. assumption. apply col_permutation_2. apply bet_col. assumption. induction H. unfold TS in H0. spliter. ex_and H2 T. assert(Col Y A T). eapply (col_transitivity_1 _ X). intro. subst Y. apply between_identity in H3. subst X. contradiction. apply col_permutation_4. apply bet_col. assumption. apply col_permutation_2. apply bet_col. assumption. apply False_ind. apply H1. apply col_permutation_2. eapply (col_transitivity_1 _ T). intro. subst T. assert(A = Y). eapply between_equality. apply between_symmetry. apply H. apply between_symmetry. assumption. subst Y. apply H1. apply col_trivial_1. apply col_permutation_4. assumption. apply col_permutation_1. assumption. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar